mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Jacobson.Ring
/-- If `K` is a Jacobson Noetherian ring, `A` a nontrivial `K`-algebra of finite type,
then any `K`-subfield of `A` is finite over `K`.  -/
RingHom.finite_of_algHom_finiteType_of_isJacobsonRing : ∀ {K : Type u_1} {L : Type u_2} {A : Type u_3} [inst : CommRing K] [inst_1 : Field L] [inst_2 : CommRing A]
  [IsJacobsonRing K] [IsNoetherianRing K] [Nontrivial A] (f : K →+* L) (g : L →+* A), (g.comp f).FiniteType → f.Finite
-- Mathlib.Algebra.Order.Hom.Basic
/-- The image of one is zero.  -/
GroupSeminormClass.map_one_eq_zero : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Group α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : GroupSeminormClass F α β] (f : F), f 1 = 0
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.instInhabitedPartialFixpoint : Inhabited Lean.Elab.PartialFixpoint
-- Mathlib.CategoryTheory.Limits.Types.Equalizers
CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype_apply : ∀ {Y Z : Type u} (g h : Y ⟶ Z) (x : CategoryTheory.Limits.equalizer g h),
  ↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.equalizerIso g h).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.equalizer.ι g h)) x
-- Mathlib.Order.Iterate
Function.Commute.iterate_pos_lt_of_map_lt : ∀ {α : Type u_1} [inst : Preorder α] {f g : α → α},
  Function.Commute f g → Monotone f → StrictMono g → ∀ {x : α}, f x < g x → ∀ {n : ℕ}, 0 < n → f^[n] x < g^[n] x
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.boundedVariation_ofDual : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  BoundedVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s) ↔ BoundedVariationOn f s
-- Mathlib.Order.Interval.Set.InitialSeg
Set.initialSegIic_toFun : ∀ {α : Type u_1} [inst : Preorder α] (j : α) (j_1 : ↑(Set.Iic j)), (Set.initialSegIic j) j_1 = ↑j_1
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.comp_apply : ∀ {X Y Z : NonemptyFinLinOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toLinOrd),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Lean.Meta.Tactic.Simp.Simproc
/-- Builtin symbolic evaluation procedures.  -/
Lean.Meta.Simp.builtinSEvalprocsRef : IO.Ref Lean.Meta.Simprocs
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.codExtend'_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Bundle.Trivialization F proj)
  [inst_3 : Nonempty (B → F → Z)],
  (Bundle.Trivialization.codExtend' hs e).baseSet = Subtype.val '' e.toPretrivialization.baseSet
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.exists_norm_eq_of_isOfFinAddOrder : ∀ {p : ℝ} [hp : Fact (0 < p)] {u : AddCircle p}, IsOfFinAddOrder u → ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))
-- Mathlib.Topology.MetricSpace.Basic
SeparationQuotient.instDist : {α : Type u} → [inst : PseudoMetricSpace α] → Dist (SeparationQuotient α)
-- Mathlib.RingTheory.WittVector.Truncated
/-- Given compatible ring homs from `S` into `TruncatedWittVector n` for each `n`, we can lift these
to a ring hom `S → 𝕎 R`.

`lift` defines the universal property of `𝕎 R` as the inverse limit of `TruncatedWittVector n`.
 -/
WittVector.lift : {p : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] →
      [inst_1 : Fact (Nat.Prime p)] →
        {S : Type u_2} →
          [inst_2 : Semiring S] →
            (f : (k : ℕ) → S →+* TruncatedWittVector p k R) →
              (∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁) →
                S →+* WittVector p R
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C),
  (CategoryTheory.CategoryStruct.id A).hom.hom = CategoryTheory.CategoryStruct.id A.X
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.map_inf : ∀ {α : Type u_1} {β : Type u_2} {m₁ m₂ : MeasurableSpace α} {f : α → β},
  MeasurableSpace.map f (m₁ ⊓ m₂) = MeasurableSpace.map f m₁ ⊓ MeasurableSpace.map f m₂
-- Mathlib.Order.Hom.Bounded
TopHom.instMin : {α : Type u_2} →
  {β : Type u_3} → [inst : Top α] → [inst_1 : SemilatticeInf β] → [inst_2 : OrderTop β] → Min (TopHom α β)
-- Init.Prelude
/-- The quotation context name for `MonadQuotation.getContext`.  -/
Lean.Macro.Context.quotContext : Lean.Macro.Context → Lean.Name
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff : ∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso] {X Y X' Y' : AlgebraicGeometry.Scheme}
  {f : X ⟶ Y} {f' : X' ⟶ Y'} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
  {h : AlgebraicGeometry.IsAffine Y}, P f ↔ P f'
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.lift_of : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  {f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {P : Type u₁} [inst_5 : L.Structure P]
  (g : (i : ι) → L.Embedding (G i) P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x)
  {i : ι} (x : G i),
  (FirstOrder.Language.DirectLimit.lift L ι G f g Hg) ((FirstOrder.Language.DirectLimit.of L ι G f i) x) = (g i) x
-- Mathlib.Order.WithBot
WithBot.lt_def_aux : ∀ {α : Type u_1} [inst : LT α] (a a_1 : WithBot α),
  a.LT a_1 ↔ (∃ b, a = ⊥ ∧ a_1 = ↑b) ∨ ∃ a_2 b, a_2 < b ∧ a = ↑a_2 ∧ a_1 = ↑b
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.norm_num_ext.sModNatTR.go.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (n acc : ℕ) (h_1 : (acc : ℕ) → motive 0 acc) (h_2 : (n acc : ℕ) → motive n.succ acc),
  (match n.succ, acc with
    | 0, acc => h_1 acc
    | n.succ, acc => h_2 n acc) =
    h_2 n acc
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k : α} [inst_3 : Inhabited (β k)],
  (List.map Sigma.fst l).contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).get! k = default
-- Mathlib.LinearAlgebra.Prod
/-- Given a linear map `f : E →ₗ[R] F` and a complement `C` of its kernel, we get a linear
equivalence between `C` and `range f`.  -/
LinearMap.kerComplementEquivRange : {R : Type u_3} →
  {M : Type u_4} →
    {M₂ : Type u_5} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M] →
              [inst_4 : Module R M₂] → (f : M →ₗ[R] M₂) → {C : Submodule R M} → IsCompl C f.ker → ↥C ≃ₗ[R] ↥f.range
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.union_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp}, t₁.union t₂ = t₁ ∪ t₂
-- Mathlib.Data.Nat.Bitwise
Nat.xor_trichotomy : ∀ {a b c : ℕ}, a ^^^ b ^^^ c ≠ 0 → b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- See `card_le_card_mul_right` for a more convenient but less general version for types with a
right-cancellative multiplication.
 -/
Finset.card_le_card_mul_right_of_injective : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α} {a : α},
  a ∈ t → IsRightRegular a → s.card ≤ (s * t).card
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → fderiv 𝕜 (f - g) x = fderiv 𝕜 f x - fderiv 𝕜 g x
-- Mathlib.Data.Sym.Sym2.Order
Sym2.sortEquiv_symm_apply : ∀ {α : Type u_1} [inst : LinearOrder α] (p : { p // p.1 ≤ p.2 }), Sym2.sortEquiv.symm p = s((↑p).1, (↑p).2)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toLp_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α}, MeasureTheory.SimpleFunc.toLp 0 ⋯ = 0
-- Mathlib.Analysis.Normed.Group.Basic
dist_zero_right : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), dist a 0 = ‖a‖
-- Mathlib.Topology.Algebra.Group.Basic
/-- Conjugation by a fixed element is continuous when `mul` is continuous.  -/
IsTopologicalGroup.continuous_conj : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : Mul G] [SeparatelyContinuousMul G] (g : G),
  Continuous fun h => g * h * g⁻¹
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.apply_mem : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} {a : α}, P.IsRepFun f → a ∈ u → f a ∈ u
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.Nil.append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w}, p.Nil → q.Nil → (p.append q).Nil
-- Mathlib.Data.Set.Function
Set.SurjOn.leftInvOn_of_rightInvOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
  Set.SurjOn f s t → Set.RightInvOn f f' s → Set.LeftInvOn f f' t
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.instIsGEObjSingleFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : C) (n : ℤ), ((DerivedCategory.singleFunctor C n).obj X).IsGE n
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_toReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → (∀ᵐ (x : α) ∂μ, f x < ⊤) → ∫ (a : α), (f a).toReal ∂μ = (∫⁻ (a : α), f a ∂μ).toReal
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instInterOfTransCmp : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Inter (Std.ExtDTreeMap α β cmp)
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.augmentedCechNerve_map_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y),
  (CategoryTheory.SimplicialObject.augmentedCechNerve.map F).right = CategoryTheory.Arrow.Hom.right F
-- Std.Data.DHashMap.Internal.AssocList.Basic
_private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.toList.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Std.DHashMap.Internal.AssocList α β → Sort u_3) (a : α) (b : β a)
  (es : Std.DHashMap.Internal.AssocList α β) (h_1 : Unit → motive Std.DHashMap.Internal.AssocList.nil)
  (h_2 :
    (a : α) →
      (b : β a) → (es : Std.DHashMap.Internal.AssocList α β) → motive (Std.DHashMap.Internal.AssocList.cons a b es)),
  (match Std.DHashMap.Internal.AssocList.cons a b es with
    | Std.DHashMap.Internal.AssocList.nil => h_1 ()
    | Std.DHashMap.Internal.AssocList.cons a b es => h_2 a b es) =
    h_2 a b es
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKey?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {k : α}, t₁.getKey? k = t₂.getKey? k
-- Lean.Environment
Lean.Environment.getModuleIdx? : Lean.Environment → Lean.Name → Option Lean.ModuleIdx
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes_stalkFunctor_map_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) {F_1 : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory C F_1]
  (x_1 : carrier (F.stalk y)),
  (CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f))
      ((CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h)) x_1) =
    (CategoryTheory.ConcreteCategory.hom (G.stalkSpecializes h))
      ((CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C y).map f)) x_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.stdSimplexHomeomorphI_symm_one : TopCat.stdSimplexHomeomorphI.symm 1 = stdSimplex.vertex 1
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- A `Triplet` over `f : X ⟶ S` and `g : Y ⟶ S` is a triple of points `x : X`, `y : Y`,
`s : S` such that `f x = s = f y`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet : {X Y S : AlgebraicGeometry.Scheme} → (X ⟶ S) → (Y ⟶ S) → Type u
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.sound : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β},
  m₁.Equiv m₂ → Std.ExtDHashMap.mk m₁ = Std.ExtDHashMap.mk m₂
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.eulerMascheroniSeq_lt_eulerMascheroniSeq' : ∀ (m n : ℕ), Real.eulerMascheroniSeq m < Real.eulerMascheroniSeq' n
-- Mathlib.Algebra.Order.Floor.Extended
/-- Extension for the `positivity` tactic: `ENat.ceil` is positive if its input is.  -/
Mathlib.Meta.Positivity.evalENatCeil : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.Multiset.Bind
Multiset.zero_bind : ∀ {α : Type u_1} {β : Type v} (f : α → Multiset β), Multiset.bind 0 f = 0
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.zeroX_eq_X : ∀ {R : Type u_1} [inst : CommRing R] (F : FormalGroup R), F.zeroX = PowerSeries.X
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_of_not_le : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ENNReal},
  ¬mΩ ≤ mΩ₀ → P⁻[X | mΩ] = 0
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.eq_of_eq_counts : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {a b : Associates α},
  a ≠ 0 → b ≠ 0 → (∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors) → a = b
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- **Alias** of `MeromorphicOn.circleIntegrable_log_norm_of_nonneg`.

---

Variant of `MeromorphicOn.circleIntegrable_log_norm` for non-negative radii.
 -/
circleIntegrable_log_norm_meromorphicOn_of_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.sphere c R) → 0 ≤ R → CircleIntegrable (fun x => Real.log ‖f x‖) c R
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.adjoin_toSubalgebra : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E]
  (S : Set E), (IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S
-- Init.MetaTypes
/-- When `singlePass` is `true` (default: `false`), the simplifier runs through a single round of simplification,
which consists of running pre-methods, recursing using congruence lemmas, and then running post-methods.
Otherwise, when it is `false`, it iteratively applies this simplification procedure.
 -/
Lean.Meta.Simp.Config.singlePass : Lean.Meta.Simp.Config → Bool
-- Mathlib.Order.WithBot
WithBot.toDual_lt_toDual_iff : ∀ {α : Type u_1} [inst : LT α] {x y : WithBot α}, WithBot.toDual x < WithBot.toDual y ↔ y < x
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The oplax monoidal functor structure induced by a `Functor.CoreMonoidal` structure.  -/
CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal : {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 D] →
            {F : CategoryTheory.Functor C D} → F.CoreMonoidal → F.OplaxMonoidal
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : β k → β k}, (m.modify k f).size = m.size
-- Mathlib.Analysis.Normed.Module.Basic
instNonUnitalNormedRingRestrictScalars : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} → {E : Type u_3} → [I : NonUnitalNormedRing E] → NonUnitalNormedRing (RestrictScalars 𝕜 𝕜' E)
-- Mathlib.Geometry.Manifold.Algebra.SMul
instContMDiffVAddOfTopWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : VAdd G M] {n : WithTop ℕ∞}
  [ContMDiffVAdd I I' ⊤ G M], ContMDiffVAdd I I' n G M
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instLetDecl : List Lean.Name →
  List Lean.Level →
    Lean.Compiler.LCNF.LetDecl Lean.Compiler.LCNF.Purity.pure →
      Lean.Compiler.LCNF.LetDecl Lean.Compiler.LCNF.Purity.pure
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
isUniformGroup_of_commGroup : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G], IsUniformGroup G
-- Mathlib.Data.Finsupp.ToDFinsupp
DFinsupp.toFinsupp_sub : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddGroup M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f g : Π₀ (x : ι), M), (f - g).toFinsupp = f.toFinsupp - g.toFinsupp
-- Mathlib.Algebra.Homology.Single
/-- The functor `V ⥤ ChainComplex V ℕ` creating a chain complex supported in degree zero.  -/
ChainComplex.single₀ : (V : Type u) →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [CategoryTheory.Limits.HasZeroObject V] → CategoryTheory.Functor V (ChainComplex V ℕ)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatWeekdayNarrow : Std.Time.DateFormatSymbols → Std.Time.Weekday → String
-- Init.Data.SInt.Lemmas
Int32.neg_mul_comm : ∀ (a b : Int32), -a * b = a * -b
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `ω ^ ω ^ … ^ 0 < ε₀`  -/
Ordinal.iterate_omega0_opow_lt_epsilon_zero : ∀ (n : ℕ), (fun a => Ordinal.omega0 ^ a)^[n] 0 < Ordinal.epsilon 0
-- Mathlib.GroupTheory.PresentedGroup
/-- The generators of a presented group generate the presented group. That is, the subgroup closure
of the set of generators equals `⊤`.  -/
PresentedGroup.closure_range_of : ∀ {α : Type u_1} (rels : Set (FreeGroup α)), Subgroup.closure (Set.range PresentedGroup.of) = ⊤
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.p_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A],
  CategoryTheory.CategoryStruct.comp P.p CategoryTheory.Limits.prod.fst = P.p₀
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceLE : Lean.Meta.Simp.Simproc
-- Lean.Elab.Util
Lean.Elab.mkMacroAttribute : Lean.Name → IO (Lean.KeyedDeclsAttribute Lean.Macro)
-- Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
/-- Infinitely smooth functions are dense in the space of continuous functions.  -/
ContinuousMap.dense_setOfPred_contDiff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F], Dense {f | ContDiff ℝ ↑⊤ ⇑f}
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.map_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms],
  CategoryTheory.Limits.Cofork.π (c.map G) = G.map (CategoryTheory.Limits.Cofork.π c)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.SL2_inv_expl_det : ∀ {R : Type v} [inst : CommRing R] (A : Matrix.SpecialLinearGroup (Fin 2) R),
  Matrix.det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1
-- Mathlib.Topology.Sheaves.Limits
TopCat.instHasColimitsOfShapePresheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{v_1, w} J]
  [CategoryTheory.Limits.HasColimitsOfShape J C] (X : TopCat),
  CategoryTheory.Limits.HasColimitsOfShape J (TopCat.Presheaf C X)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.compare_getKey_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} (h' : k ∈ t), cmp (t.getKey k h') k = Ordering.eq
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.tanh_surjOn : Set.SurjOn Real.tanh Set.univ (Set.Ioo (-1) 1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.inclusion.coe_eq : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : MulAction M α] (s : SubMulAction M α),
  ⇑s.inclusion = Subtype.val
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- Given a vertex in the support of a path, give the path from (and including) that vertex to
the end. In other words, drop vertices from the front of a path until (and not including)
that vertex.  -/
SimpleGraph.Walk.dropUntil : {V : Type u} →
  {G : SimpleGraph V} → [DecidableEq V] → {v w : V} → (p : G.Walk v w) → (u : V) → u ∈ p.support → G.Walk u w
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_eval₂_eq_zero : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : CommSemiring S] {p : Polynomial R} (f : R →+* S) {z : S},
  Polynomial.eval₂ f z p = 0 →
    (∀ (x : R), f x = 0 → x = 0) → Polynomial.eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C),
  AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso.inv.app X =
    CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)
-- Init.Data.Array.Lemmas
Array.forall_mem_iff_forall_getElem : ∀ {α : Type u_1} {P : α → Prop} {xs : Array α}, (∀ x ∈ xs, P x) ↔ ∀ (i : ℕ) (hi : i < xs.size), P xs[i]
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- the functor preserves the cokernel of `S.f : S.X₁ ⟶ S.X₂`.  -/
CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.f : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C}
  {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData)
  {F : CategoryTheory.Functor C D} {inst_4 : F.PreservesZeroMorphisms} [self : h.IsPreservedBy F],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F
-- Mathlib.Order.Filter.Pointwise
Filter.le_smul_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g h : Filter β},
  h ≤ f • g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s • t ∈ h