mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)}
  (app app_1 : (c : C) → A.obj c → (F.obj c ⟶ G.obj c)) (e_app : app = app_1)
  (naturality :
    ∀ {c d : C} (f : c ⟶ d) (a : A.obj c),
      CategoryTheory.CategoryStruct.comp (F.map f) (app d ((CategoryTheory.ConcreteCategory.hom (A.map f)) a)) =
        CategoryTheory.CategoryStruct.comp (app c a) (G.map f)),
  { app := app, naturality := naturality } = { app := app_1, naturality := ⋯ }
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.cooper_unsat'_helper : ∀ {a b d c k x : ℤ}, d > 0 → x = k * d + c → a ≤ x → x ≤ b → ¬b < Int.Internal.Linear.cdiv (a - c) d * d + c
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.aeval_X_left_eq_algebraMap : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K),
  (Polynomial.aeval RatFunc.X) p = (algebraMap (Polynomial K) (RatFunc K)) p
-- Mathlib.Topology.VectorBundle.Basic
ContinuousLinearMap.inCoordinates.congr_simp : ∀ {B : Type u_2} (F : Type u_3) (E : B → Type u_4) [inst : (x : B) → AddCommMonoid (E x)]
  [inst_1 : NormedAddCommGroup F] [inst_2 : TopologicalSpace B] [inst_3 : (x : B) → TopologicalSpace (E x)]
  {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} [inst_4 : NontriviallyNormedField 𝕜₁] [inst_5 : NontriviallyNormedField 𝕜₂]
  {σ : 𝕜₁ →+* 𝕜₂} {B' : Type u_7} [inst_6 : TopologicalSpace B'] [inst_7 : NormedSpace 𝕜₁ F]
  [inst_8 : (x : B) → Module 𝕜₁ (E x)] [inst_9 : TopologicalSpace (Bundle.TotalSpace F E)] (F' : Type u_8)
  [inst_10 : NormedAddCommGroup F'] [inst_11 : NormedSpace 𝕜₂ F'] (E' : B' → Type u_9)
  [inst_12 : (x : B') → AddCommMonoid (E' x)] [inst_13 : (x : B') → Module 𝕜₂ (E' x)]
  [inst_14 : TopologicalSpace (Bundle.TotalSpace F' E')] [inst_15 : FiberBundle F E] [inst_16 : VectorBundle 𝕜₁ F E]
  [inst_17 : (x : B') → TopologicalSpace (E' x)] [inst_18 : FiberBundle F' E'] [inst_19 : VectorBundle 𝕜₂ F' E']
  (x₀ x₀_1 : B),
  x₀ = x₀_1 →
    ∀ (x : B) (y₀ y₀_1 : B'),
      y₀ = y₀_1 →
        ∀ (y : B') (ϕ ϕ_1 : E x →SL[σ] E' y),
          ϕ = ϕ_1 →
            ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ =
              ContinuousLinearMap.inCoordinates F E F' E' x₀_1 x y₀_1 y ϕ_1
-- Mathlib.Data.Seq.Computation
Computation.map_congr : ∀ {α : Type u} {β : Type v} {s1 s2 : Computation α} {f : α → β},
  s1.Equiv s2 → (Computation.map f s1).Equiv (Computation.map f s2)
-- Mathlib.Analysis.Convex.Body
/-- **Alias** of `ConvexBody.hausdorffEDist_coe`. -/
ConvexBody.hausdorffEdist_coe : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (K L : ConvexBody V),
  Metric.hausdorffEDist ↑K ↑L = edist K L
-- Mathlib.Data.ENNReal.Operations
ENNReal.sInf_add : ∀ {a : ENNReal} {s : Set ENNReal}, sInf s + a = ⨅ b ∈ s, b + a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_insertIfNew_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).size ≤ t.size + 1
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.instHasLimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{v_1, w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Mon C)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {T : CategoryTheory.Monad C} {c c' : CategoryTheory.Kleisli T}
  {of of_1 : c.of ⟶ T.obj c'.of}, { of := of } = { of := of_1 } → of = of_1
-- Mathlib.Data.Stream.Init
Stream'.map_eq : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream' α),
  Stream'.map f s = Stream'.cons (f s.head) (Stream'.map f s.tail)
-- Lean.Language.Basic
Lean.Language.ToSnapshotTree.mk : {α : Type} → (α → Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree) → Lean.Language.ToSnapshotTree α
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Range.mk.injEq : ∀ (start «end» start_1 end_1 : Lean.Lsp.Position),
  ({ start := start, «end» := «end» } = { start := start_1, «end» := end_1 }) = (start = start_1 ∧ «end» = end_1)
-- Mathlib.Topology.Homotopy.Lifting
/-- **Alias** of the forward direction of `IsAddQuotientCoveringMap.monodromy_ext_iff`. -/
IsAddQuotientCoveringMap.monodromy_ext : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x y : X}
  {γ γ' : Path.Homotopic.Quotient x y} (e : ↑(p ⁻¹' {x})),
  ⋯.monodromy γ e = ⋯.monodromy γ' e → ⋯.monodromy γ = ⋯.monodromy γ'
-- Lean.Parser.Module
Lean.Parser.ModuleParserState.mk.sizeOf_spec : ∀ (pos : String.Pos.Raw) (recovering hasLeading : Bool),
  sizeOf { pos := pos, recovering := recovering, hasLeading := hasLeading } =
    1 + sizeOf pos + sizeOf recovering + sizeOf hasLeading
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq_measurableSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α} (n : ℕ),
  MeasurableSet (MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i n)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.IsInner.mk : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore},
  (∀ (s : h.ι), h.index s ≠ 0) → (∀ (s : h.ι), h.index s ≠ Fin.last (h.dim s + 1)) → h.IsInner
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, local version for any measure.
Let filters `l` and `l'` be related by `TendstoIxxClass Ioc`.
If `f` has a finite limit `c` at `l ⊓ ae μ`, where `μ` is a measure
finite at `l`, then `∫ x in u..v, f x ∂μ = μ (Ioc u v) • c + o(μ(Ioc u v))` as both
`u` and `v` tend to `l` so that `u ≤ v`.

See also `measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le` for a version assuming
`[intervalIntegral.FTCFilter a l l']` and `[MeasureTheory.IsLocallyFiniteMeasure μ]`. If `l` is one
of `𝓝[≥] a`, `𝓝[≤] a`, `𝓝 a`, then it's easier to apply the non-primed version.  The primed version
also works, e.g., for `l = l' = Filter.atTop`.  -/
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {c : E}
  {l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [CompleteSpace E]
  [l'.IsMeasurablyGenerated] [Filter.TendstoIxxClass Set.Ioc l l'],
  StronglyMeasurableAtFilter f l' μ →
    Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c) →
      μ.FiniteAtFilter l' →
        Filter.Tendsto u lt l →
          Filter.Tendsto v lt l →
            u ≤ᶠ[lt] v →
              (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - μ.real (Set.Ioc (u t) (v t)) • c) =o[lt] fun t =>
                μ.real (Set.Ioc (u t) (v t))
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- The extension of a family agrees with the original family.  -/
CategoryTheory.Presieve.extend_agrees : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R},
  x.Compatible → ∀ {f : Y ⟶ X} (hf : R f), x.sieveExtend f ⋯ = x f hf
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.rev_map_σ : ∀ {n : ℕ} (i : Fin (n + 1)), SimplexCategory.rev.map (SimplexCategory.σ i) = SimplexCategory.σ i.rev
-- Init.Data.BitVec.Lemmas
BitVec.getElem_concat_succ : ∀ {w : ℕ} {b : Bool} {x : BitVec w} {i : ℕ} (h : i + 1 < w + 1), (x.concat b)[i + 1] = x[i]
-- Lean.Parser.Command
Lean.Parser.Command.opaque : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.Functor.toPseudofunctor'_mapComp : ∀ {I : Type u_1} {B : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} I] [inst_1 : CategoryTheory.Bicategory B]
  [inst_2 : CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B)
  {a b c : CategoryTheory.LocallyDiscrete I} (f : a ⟶ b) (g : b ⟶ c),
  F.toPseudofunctor'.mapComp f g = CategoryTheory.eqToIso ⋯
-- Lean.Meta.Tactic.Ext
/-- Returns `true` if `declName` is tagged with `[ext]` attribute.  -/
Lean.Meta.Ext.isExtTheorem : Lean.Name → Lean.CoreM Bool
-- Lean.Elab.Command
_private.Lean.Elab.Command.0.Lean.Elab.Command.mkInfoTree : Lean.Name → Lean.Syntax → Lean.PersistentArray Lean.Elab.InfoTree → Lean.Elab.Command.CommandElabM Lean.Elab.InfoTree
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SFinite ν] (s : Set α),
  ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν)).real s
-- Init.Data.Nat.Lemmas
Nat.eq_one_of_mul_eq_one_right : ∀ {m n : ℕ}, m * n = 1 → m = 1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_comap : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (S : Subsemigroup P)
  (g : N →ₙ* P) (f : M →ₙ* N), Subsemigroup.comap f (Subsemigroup.comap g S) = Subsemigroup.comap (g.comp f) S
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.ofList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, Std.TreeSet.ofList [k] cmp = ∅.insert k
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply : ∀ (M : Type u_1) [inst : Monoid M] {X : Type u} [inst_1 : MulAction M X] (x : X) (f : CategoryTheory.End ⟨(), x⟩),
  (CategoryTheory.ActionCategory.stabilizerIsoEnd M x).symm f = f
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : C},
  (∀ {X Y : C} (g : X ⟶ J) (f : X ⟶ Y) [CategoryTheory.Mono f], ∃ h, CategoryTheory.CategoryStruct.comp f h = g) →
    CategoryTheory.Injective J
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.isScalarTower'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α β] [inst_1 : SMul α γ] [inst_2 : SMul β γ]
  [IsScalarTower α β γ], IsScalarTower (Set α) (Set β) (Set γ)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Subfield.isTotallyReal_bot : ∀ (K : Type u_2) [inst : Field K] [CharZero K], NumberField.IsTotallyReal ↥⊥
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.instFaithfulObjCompPost : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D), (CategoryTheory.StructuredArrow.post S F G).Faithful
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.wellPowered : ∀ {C₀ : Type u} [inst : CategoryTheory.SmallCategory C₀] (R₀ : CategoryTheory.Functor C₀ᵒᵖ RingCat),
  CategoryTheory.WellPowered.{u, u, u + 1} (PresheafOfModules R₀)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.mk : {R : Type u_1} → {a b c : R} → R → R → R → R → QuaternionAlgebra R a b c
-- Mathlib.GroupTheory.HNNExtension
/-- Define a function `HNNExtension G A B φ →* H`, by defining it on `G` and `t`  -/
HNNExtension.lift : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      {φ : ↥A ≃* ↥B} →
        {H : Type u_2} →
          [inst_1 : Group H] →
            (f : G →* H) → (x : H) → (∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x) → HNNExtension G A B φ →* H
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionParams.mk.sizeOf_spec : ∀ (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (toPartialResultParams : Lean.Lsp.PartialResultParams)
  (textDocument : Lean.Lsp.TextDocumentIdentifier) (range : Lean.Lsp.Range) (context : Lean.Lsp.CodeActionContext),
  sizeOf
      { toWorkDoneProgressParams := toWorkDoneProgressParams, toPartialResultParams := toPartialResultParams,
        textDocument := textDocument, range := range, context := context } =
    1 + sizeOf toWorkDoneProgressParams + sizeOf toPartialResultParams + sizeOf textDocument + sizeOf range +
      sizeOf context
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_Ioi_natAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.natAdd m ⁻¹' Set.Ioi (Fin.natAdd m i) = Set.Ioi i
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The canonical pullback cone from the data of a chosen pullback of `f` along `g`.  -/
CategoryTheory.ChosenPullbacksAlong.pullbackCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} →
      (f : Y ⟶ X) → (g : Z ⟶ X) → [CategoryTheory.ChosenPullbacksAlong g] → CategoryTheory.Limits.PullbackCone f g
-- Mathlib.GroupTheory.Coset.Basic
mem_leftCoset : ∀ {α : Type u_1} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → a * x ∈ a • s
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.descOfIsLeftKanExtension.congr_simp : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α α_1 : F ⟶ L.comp F') (e_α : α = α_1) [inst_3 : F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H)
  (β β_1 : F ⟶ L.comp G), β = β_1 → F'.descOfIsLeftKanExtension α G β = F'.descOfIsLeftKanExtension α_1 G β_1
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_bodd : Primrec Nat.bodd
-- Mathlib.CategoryTheory.Abelian.Basic
/-- A category with finite products in which coimage-image comparisons are all isomorphisms
is a normal epi category.
 -/
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.isNormalEpiCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)]
  [CategoryTheory.Limits.HasFiniteProducts C], CategoryTheory.IsNormalEpiCategory C
-- Mathlib.Order.BooleanAlgebra.Basic
codisjoint_himp_self_left : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], Codisjoint (x ⇨ y) x
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_iInf : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {ι : Sort u_1} {S : ι → NonUnitalSubsemiring R} {x : R},
  x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.Order.Category.Preord
/-- The category of preorders.  -/
Preord : Type (u_1 + 1)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableAt.add_iff_left` -/
DifferentiableAt.fun_add_iff_left : ∀ {𝕜 : 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 𝕜 g x → (DifferentiableAt 𝕜 (fun i => f i + g i) x ↔ DifferentiableAt 𝕜 f x)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.replaceMainGoal : List Lean.Meta.Grind.Goal → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Lean.Data.PersistentArray
Lean.PersistentArray.toList : {α : Type u} → Lean.PersistentArray α → List α
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.pullback_χ_obj_mk_truth`. -/
CategoryTheory.Classifier.pullback_χ_obj_mk_truth : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (𝒞 : CategoryTheory.Subobject.Classifier C) {Z X : C} (i : Z ⟶ X) [inst_2 : CategoryTheory.Mono i],
  (CategoryTheory.Subobject.pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject = CategoryTheory.Subobject.mk i
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.roots_eq_zero_iff_degree_nonpos : ∀ {k : Type u} [inst : Field k] [IsAlgClosed k] {p : Polynomial k}, p.roots = 0 ↔ p.degree ≤ 0
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map_one : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (f : R →+* S), MonoidAlgebra.map (↑f) 1 = 1
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.mem_support_ofFintype_iff : ∀ {α : Type u_1} [inst : Fintype α] {f : α → ENNReal} (h : ∑ a, f a = 1) (a : α),
  a ∈ (PMF.ofFintype f h).support ↔ f a ≠ 0
-- Mathlib.RingTheory.Adjoin.PowerBasis
PowerBasis.ofAdjoinEqTop_gen : ∀ {K : Type u_1} {S : Type u_2} [inst : Field K] [inst_1 : CommRing S] [inst_2 : Algebra K S] {x : S}
  (hx : IsIntegral K x) (hx' : K[x] = ⊤), (PowerBasis.ofAdjoinEqTop hx hx').gen = x
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.mk.inj : ∀ {M : Type u_10} {N : Type u_11} {inst : Mul M} {inst_1 : Mul N} {toFun : M → N}
  {map_mul' : ∀ (x y : M), toFun (x * y) = toFun x * toFun y} {toFun_1 : M → N}
  {map_mul'_1 : ∀ (x y : M), toFun_1 (x * y) = toFun_1 x * toFun_1 y},
  { toFun := toFun, map_mul' := map_mul' } = { toFun := toFun_1, map_mul' := map_mul'_1 } → toFun = toFun_1
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.ensureArgType : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.revSkipWhile_cast : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy) {pos : s.Pos},
  (pos.cast hst).revSkipWhile pat = (pos.revSkipWhile pat).cast hst
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.instIsFiniteMeasureOnCompactsComapComplexCoeVolume : MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProduct_isoClosure_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P Q : CategoryTheory.ObjectProperty C), P.isoClosure.extensionProduct Q = P.extensionProduct Q
-- Mathlib.Algebra.Ring.CharZero
CharZero.neg_eq_self_iff : ∀ {R : Type u_2} [inst : NonAssocRing R] [NoZeroDivisors R] [CharZero R] {a : R}, -a = a ↔ a = 0
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.pow : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Monoid β] [ContinuousMul β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f ^ n) μ
-- Mathlib.GroupTheory.GroupAction.Jordan
_private.Mathlib.GroupTheory.GroupAction.Jordan.0.is_two_preprimitive_strong_jordan : {G : Type u_1} →
  {α : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G α] →
        MulAction.IsPreprimitive G α →
          {s : Set α} →
            {n : ℕ} →
              s.ncard = n + 1 →
                n + 2 < Nat.card α →
                  MulAction.IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
                    ProofWanted (MulAction.IsMultiplyPreprimitive (↥(Subgroup.normalClosure ↑(fixingSubgroup G s))) α 2)
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.setIntegral_compProd_univ_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] (f : β × γ → E) {t : Set γ},
  MeasurableSet t →
    MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ((κ.compProd η) a) →
      ∫ (z : β × γ) in Set.univ ×ˢ t, f z ∂(κ.compProd η) a = ∫ (x : β), ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The diagram of finite quotients indexed by finite-index normal subgroups.  -/
ProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagram : (G : AddGrpCat) → CategoryTheory.Functor (FiniteIndexNormalAddSubgroup ↑G) FiniteAddGrp.{u}
-- Init.Data.Range.Polymorphic.Map
Std.PRange.instPreservesLTOfLawfulOrderLTOfPreservesLE : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : LE α] [inst_3 : LT α] [Std.LawfulOrderLT α] [inst_5 : LE β] [inst_6 : LT β] [Std.LawfulOrderLT β]
  (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLE], f.PreservesLT
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.forget_obj : ∀ {R : Type u} [inst : CommRing R] (A : CommHopfAlgCat R), (CategoryTheory.forget (CommHopfAlgCat R)).obj A = ↑A
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- An affine subspace contains zero if and only if it equals its directions.  -/
AffineSubspace.direction_eq_self_iff_zero_mem : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  {s : AffineSubspace k V}, ↑s.direction = s ↔ 0 ∈ s
-- Mathlib.Data.DFinsupp.Order
DFinsupp.le_iff' : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : DecidableEq ι] [inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)]
  {f g : Π₀ (i : ι), α i} {s : Finset ι}, f.support ⊆ s → (f ≤ g ↔ ∀ i ∈ s, f i ≤ g i)
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.base.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {ι : C → Type w} (X : C)
  (a a_1 : ι X),
  (CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ X a =
      CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ X a_1) =
    (a = a_1)
-- Mathlib.Algebra.Group.Prod
Prod.instAddCommMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N],
  Prod.instAddCommMonoid = { toAddMonoid := Prod.instAddMonoid, add_comm := ⋯ }
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_subst_finite : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a →
    ∀ (f : PowerSeries R) (e : τ →₀ ℕ),
      Function.HasFiniteSupport fun d => (PowerSeries.coeff d) f • (MvPowerSeries.coeff e) (a ^ d)
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.det_fintype : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [inst : CommRing R] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : DecidableEq α] [inst_4 : Fintype α] [inst_5 : LinearOrder α],
  M.BlockTriangular b → M.det = ∏ k, (M.toSquareBlock b k).det
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Iic_of_monotoneOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Iic a) →
    MonotoneOn f (Set.Iic a) → Filter.Tendsto f Filter.atBot Filter.atBot → f '' Set.Iic a = Set.Iic (f a)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_pos : ∀ {b x : ℝ}, 1 < b → 1 < x → 0 < Real.logb b x
-- Mathlib.Algebra.Group.Equiv.Basic
Equiv.neg.eq_1 : ∀ (G : Type u_14) [inst : InvolutiveNeg G], Equiv.neg G = Function.Involutive.toPerm Neg.neg ⋯