mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.instSFiniteHAddMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν], MeasureTheory.SFinite (μ + ν)
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.eval_eq_sum_range' : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ},
  p.natDegree < n → ∀ (x : R), Polynomial.eval x p = ∑ i ∈ Finset.range n, p.coeff i * x ^ i
-- Init.Data.SInt.Lemmas
Int64.toInt8_toInt32 : ∀ (n : Int64), n.toInt32.toInt8 = n.toInt8
-- Mathlib.RingTheory.Localization.Module
LocalizedModule.map_injective : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {N : Type u_3} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (l : M →ₗ[R] N),
  Function.Injective ⇑l → Function.Injective ⇑((LocalizedModule.map S) l)
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.dcongr_arg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_2} {F G : ι → C} (α : (i : ι) → F i ⟶ G i)
  {i j : ι} (h : i = j),
  α i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (α j) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Order.RelSeries
SetRel.not_finiteDimensional_iff : ∀ {α : Type u_1} {r : SetRel α α} [Nonempty α], ¬r.FiniteDimensional ↔ r.InfiniteDimensional
-- Mathlib.SetTheory.Lists
Lists.toList.eq_1 : ∀ {α : Type u_1} (fst : Bool) (l : Lists' α fst), Lists.toList ⟨fst, l⟩ = l.toList
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.coe_id : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α], ⇑(Dilation.id α) = id
-- Std.Http.Internal.String
/-- Attempts to quote `s` as an HTTP `quoted-string`.

Returns `some` with the quoted result when every character passes `quotedStringChar`, or `none`
when any character cannot be represented by the grammar.
 -/
Std.Http.Internal.quoteHttpString? : String → Option String
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.zero_zsmul : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.zsmul 0 a = Lean.Grind.IntModule.OfNatModule.zero
-- Mathlib.Order.Nucleus
Nucleus.instFunLike : {X : Type u_1} → [inst : SemilatticeInf X] → FunLike (Nucleus X) X X
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.connected_or_connected_compl : ∀ {V : Type u} (G : SimpleGraph V) [Nonempty V], G.Connected ∨ Gᶜ.Connected
-- Mathlib.RingTheory.IdealFilter.Topology
/-- The topology on `A` induced by `addGroupFilterBasis`.  -/
WithIdealFilter.instTopologicalSpace : {A : Type u_1} → [inst : Ring A] → {F : IdealFilter A} → TopologicalSpace (WithIdealFilter F)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) ∘ₗ
      LinearMap.baseChange T P.toExtension.cotangentComplex =
    (Q.comp P).toExtension.cotangentComplex ∘ₗ
      LinearMap.liftBaseChange T (Algebra.Extension.Cotangent.map (Q.toComp P).toExtensionHom)
-- Mathlib.Data.Nat.Log
Nat.clog_of_left_le_one : ∀ {b : ℕ}, b ≤ 1 → ∀ (n : ℕ), Nat.clog b n = 0
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.forget_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.LaxBraidedFunctor C D), CategoryTheory.LaxBraidedFunctor.forget.obj F = F.toLaxMonoidalFunctor
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.source_restr_subset_source : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α), (e.restr s).source ⊆ e.source
-- Init.Data.Nat.ToString
Nat.digitChar_eq_three : ∀ {n : ℕ}, n.digitChar = '3' ↔ n = 3
-- Mathlib.CategoryTheory.Yoneda
/-- Corepresenting objects are unique up to isomorphism.  -/
CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C (Type v)} → {X X' : C} → F.CorepresentableBy X → F.CorepresentableBy X' → (X ≅ X')
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_zero : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}), Ordinal.veblenWith f 0 = f
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Nat.Prime.log_pos : ∀ {p : ℕ}, Nat.Prime p → 0 < Real.log ↑p
-- Mathlib.Logic.Equiv.Set
Equiv.sigmaPreimageEquiv_apply : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (x : (y : β) × { x // f x = y }), (Equiv.sigmaPreimageEquiv f) x = ↑x.snd
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.Adapted.isStoppingTime_hittingAfter : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
  [WellFoundedLT ι] [Countable ι] {x : MeasurableSpace β} {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {s : Set β}
  {n : ι},
  MeasureTheory.Adapted f u → MeasurableSet s → MeasureTheory.IsStoppingTime f (MeasureTheory.hittingAfter u s n)
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_apply : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : Polynomial R),
  (Polynomial.taylor r) f = f.comp (Polynomial.X + Polynomial.C r)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symmₗ_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ∀ (y : F), (Bundle.Trivialization.symmₗ R e b) y = e.symm b y
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_eq_of_bounds : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {φ : E →SL[σ₁₂] F} {M : ℝ},
  0 ≤ M → (∀ (x : E), ‖φ x‖ ≤ M * ‖x‖) → (∀ N ≥ 0, (∀ (x : E), ‖φ x‖ ≤ N * ‖x‖) → M ≤ N) → ‖φ‖ = M
-- Init.Data.Nat.Dvd
Nat.eq_one_of_dvd_one : ∀ {n : ℕ}, n ∣ 1 → n = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Raw.Const.get? (m₁ \ m₂) k =
          if m₂.contains k = true then none else Std.DTreeMap.Raw.Const.get? m₁ k
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.hasBinaryCoproducts_of_hasBinaryBiproducts : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasBinaryBiproducts C], CategoryTheory.Limits.HasBinaryCoproducts C
-- Init.Data.String.Subslice
/-- Given a subslice `sl` of `s` and a position `newStart` that is at most the
start position of the subslice, obtain a new subslice whose start is `newStart` and whose
end is the end of `sl`.
 -/
String.Slice.Subslice.extendLeft : {s : String.Slice} → (sl : s.Subslice) → (newStart : s.Pos) → newStart ≤ sl.startInclusive → s.Subslice
-- Mathlib.Topology.UniformSpace.Compact
Filter.HasBasis.lebesgue_number_lemma_nhds' : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {ι' : Sort u_2} {p : ι' → Prop} {V : ι' → Set (α × α)}
  {U : (x : α) → x ∈ K → Set α},
  (uniformity α).HasBasis p V →
    IsCompact K →
      (∀ (x : α) (hx : x ∈ K), U x hx ∈ nhds x) → ∃ i, p i ∧ ∀ x ∈ K, ∃ y, UniformSpace.ball x (V i) ⊆ U ↑y ⋯
-- Mathlib.Data.Fin.Parity
/-- In `Fin n`, all elements are odd for odd `n`,
otherwise an element is odd iff its `Fin.val` value is odd.  -/
Fin.odd_iff : ∀ {n : ℕ} {k : Fin n} [inst : NeZero n], Odd k ↔ Odd n ∨ Odd ↑k
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_expand_pow_map_iterateFrobenius : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p n : ℕ} [inst_2 : ExpChar R p] {f : Polynomial R}
  [PerfectRing R p], Multiset.map (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots = p ^ n • f.roots
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.findIdx.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) → ((n : ℕ) → motive [] n) → ((a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n) → motive x x_1
-- Mathlib.Order.Bounded
Set.bounded_ge_Ioo : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 ≥ x2) (Set.Ioo a b)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates limits, then `F.unop : C ⥤ D` creates colimits.  -/
CategoryTheory.Limits.createsColimitsUnop : {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.CreatesLimits F] → CategoryTheory.CreatesColimits F.unop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α}, t.isEmpty = true → t.get? a = none
-- Mathlib.CategoryTheory.Localization.HasLocalization
/-- The constructed localized category.  -/
CategoryTheory.MorphismProperty.HasLocalization.standard : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (W : CategoryTheory.MorphismProperty C) → W.HasLocalization
-- Mathlib.Analysis.SpecialFunctions.Pochhammer
/-- `descPochhammer 𝕜 n` is differentiable.  -/
differentiable_descPochhammer_eval : ∀ {n : ℕ} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜],
  Differentiable 𝕜 fun x => Polynomial.eval x (descPochhammer 𝕜 n)
-- Mathlib.Order.Filter.CountableInter
Filter.CountableGenerateSets.sInter : ∀ {α : Type u_2} {g S : Set (Set α)},
  S.Countable → (∀ s ∈ S, Filter.CountableGenerateSets g s) → Filter.CountableGenerateSets g (⋂₀ S)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
StrictMono.const_mul_of_neg : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] {a : R} [inst_2 : Preorder α] {f : α → R}
  [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R],
  StrictMono f → a < 0 → StrictAnti fun x => a * f x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α},
  Std.DTreeMap.Const.get! (t₁ \ t₂) k = if k ∈ t₂ then default else Std.DTreeMap.Const.get! t₁ k
-- Init.Data.List.SplitOn.Basic
List.splitOnP.go : {α : Type u_1} → (α → Bool) → List α → List α → List (List α)
-- Mathlib.Topology.EMetricSpace.Weak
instWeakPseudoEMetricSpaceWithBot : {α : Type u} →
  [t : TopologicalSpace α] →
    [inst : LinearOrder α] →
      [inst_1 : OrderTopology α] → [m : WeakPseudoEMetricSpace α] → WeakPseudoEMetricSpace (WithBot α)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Closure of a subfield `S` equals `S`.  -/
Subfield.closure_eq : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), Subfield.closure ↑s = s
-- Mathlib.Combinatorics.Hindman
Hindman.FP.cons' : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (m : M), Hindman.FP a.tail m → Hindman.FP a (a.head * m)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits, then `F.unop : C ⥤ D` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfSizeUnop : {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.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
            CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.structureInstances.defaults : Lean.Option Bool
-- Mathlib.Algebra.Order.Group.CompleteLattice
add_ciInf : ∀ {ι : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [AddLeftMono G], BddBelow (Set.range f) → ∀ (a : G), a + ⨅ i, f i = ⨅ i, a + f i
-- Mathlib.Topology.ClusterPt
accPt_principal_iff_nhdsWithin : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X},
  AccPt x (Filter.principal s) ↔ (nhdsWithin x (s \ {x})).NeBot
-- Mathlib.Data.Seq.Basic
/-- Flatten a nonempty sequence of nonempty sequences  -/
Stream'.Seq1.join : {α : Type u} → Stream'.Seq1 (Stream'.Seq1 α) → Stream'.Seq1 α
-- Mathlib.Algebra.Ring.Subring.Order
Subring.orderedSubtype_coe : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] (s : Subring R), ↑s.orderedSubtype = s.subtype
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mk.inj : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {toPrepartition : BoxIntegral.Prepartition I} {tag : BoxIntegral.Box ι → ι → ℝ}
  {tag_mem_Icc : ∀ (J : BoxIntegral.Box ι), tag J ∈ BoxIntegral.Box.Icc I}
  {toPrepartition_1 : BoxIntegral.Prepartition I} {tag_1 : BoxIntegral.Box ι → ι → ℝ}
  {tag_mem_Icc_1 : ∀ (J : BoxIntegral.Box ι), tag_1 J ∈ BoxIntegral.Box.Icc I},
  { toPrepartition := toPrepartition, tag := tag, tag_mem_Icc := tag_mem_Icc } =
      { toPrepartition := toPrepartition_1, tag := tag_1, tag_mem_Icc := tag_mem_Icc_1 } →
    toPrepartition = toPrepartition_1 ∧ tag = tag_1
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.isUniformEmbedding_toProdMulOpposite : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A],
  IsUniformEmbedding DoubleCentralizer.toProdMulOpposite
-- Mathlib.Algebra.BigOperators.Pi
/-- Decomposing `x : ι → R` as a sum along the canonical basis `Pi.single i 1` for `i : ι`.  -/
pi_eq_sum_univ' : ∀ {ι : Type u_7} [inst : Fintype ι] [inst_1 : DecidableEq ι] {R : Type u_8} [inst_2 : NonAssocSemiring R] (x : ι → R),
  x = ∑ i, x i • Pi.single i 1
-- Mathlib.Analysis.Convex.Between
Wbtw.trans_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {w x y z : P},
  Wbtw R w x z → Wbtw R x y z → Wbtw R w y z
-- Mathlib.Data.Multiset.Filter
Multiset.filter_add_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (q : α → Prop) [inst_1 : DecidablePred q] (s : Multiset α),
  Multiset.filter p s + Multiset.filter q s =
    Multiset.filter (fun a => p a ∨ q a) s + Multiset.filter (fun a => p a ∧ q a) s
-- Mathlib.RingTheory.Teichmuller
/-- `teichmuller` as a `MonoidWithZeroHom`. This is the simp NF.  -/
Perfection.teichmuller₀ : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst_1 : CommRing R] →
        (I : Ideal R) → [inst_2 : CharP (R ⧸ I) p] → [IsAdicComplete I R] → Perfection (R ⧸ I) p →*₀ R
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- A `LightDiagram'` yields a `Profinite`.  -/
LightDiagram'.toProfinite : LightDiagram' → Profinite
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_eq_integral : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (f : α → E),
  ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ
-- Mathlib.Order.WithBot
/-- The order on `WithTop α`, defined by `↑a < ⊤` and `a < b → ↑a < ↑b`.

Equivalently, `x < y` can be defined as `∃ a : α, x = ↑a ∧ ∀ b : α, y = ↑b → a < b`,
see `le_if_forall`. The definition as an inductive predicate is preferred since it
cannot be accidentally unfolded too far.  -/
WithTop.instLT : {α : Type u_1} → [LT α] → LT (WithTop α)
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.restrict.eq_1 : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  {F : TopCat.Presheaf C X} {V : TopologicalSpace.Opens ↑X} (x : CategoryTheory.ToType (F.obj (Opposite.op V)))
  {U : TopologicalSpace.Opens ↑X} (h : U ⟶ V),
  TopCat.Presheaf.restrict x h = (CategoryTheory.ConcreteCategory.hom (F.map h.op)) x
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.instHasProjectiveDimensionLTBiprod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X Y : C) (n : ℕ)
  [CategoryTheory.HasProjectiveDimensionLT X n] [CategoryTheory.HasProjectiveDimensionLT Y n],
  CategoryTheory.HasProjectiveDimensionLT (X ⊞ Y) n
-- Mathlib.Order.Height
Set.chainHeight.eq_1 : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.chainHeight r = ⨆ t, (↑t).encard
-- Lean.Compiler.IR.Basic
/-- Arguments to applications, constructors, etc.
We use `erased` for Lean types, propositions and proofs that have been erased.
Recall that for a Function `f`, we also generate `f._rarg` which does not take
`erased` arguments. However, `f._rarg` is only safe to be used in full applications.  -/
Lean.IR.Arg : Type
-- Mathlib.RingTheory.Valuation.IsTrivialOn
/-- For an `A`-algebra `K` and a valuation `v` over `K` which is trivial on `A`.
If `y : K` is such that `y ≠ 0` and `v y ≠ 1`, then it is transcendental over `A`.  -/
Valuation.transcendental_of_ne_one : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] (A : Type u_2) [inst_1 : CommRing A] {K : Type u_3}
  [inst_2 : Field K] [inst_3 : Algebra A K] {v : Valuation K Γ} [hv : Valuation.IsTrivialOn A v] (y : K),
  y ≠ 0 → v y ≠ 1 → Transcendental A y
-- Mathlib.Order.Filter.Curry
Filter.frequently_curry_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} (p : α × β → Prop),
  (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)
-- Mathlib.Algebra.Group.End
AddAut.neg_conj_apply : ∀ {G : Type u_3} [inst : AddGroup G] (g h : G), (-AddAut.addConj g) h = -g + h + g
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
ISize.reduceToInt : Lean.Meta.Simp.Simproc
-- Aesop.Frontend.Extension
Aesop.Frontend.addGlobalRule : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [MonadLiftT IO m] →
        [MonadLiftT Lean.CoreM m] →
          [Lean.MonadEnv m] →
            [Lean.MonadResolveName m] →
              Aesop.RuleSetName → Aesop.GlobalRuleSetMember → Lean.AttributeKind → Bool → m Unit
-- Mathlib.Algebra.Group.Action.Hom
/-- If the additive action of `M` on `N` is compatible with addition on `N`, then
`fun x ↦ x +ᵥ 0` is an additive monoid homomorphism from `M` to `N`.  -/
AddMonoidHom.vaddZeroHom : {M : Type u_4} →
  {N : Type u_5} →
    [inst : AddMonoid M] → [inst_1 : AddZeroClass N] → [inst_2 : AddAction M N] → [VAddAssocClass M N N] → M →+ N
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.UsedSimps : Type
-- Std.Sync.CancellationContext
/-- Map of token IDs to optional tokens and their children.
 -/
Std.CancellationContext.State.tokens : Std.CancellationContext.State → Std.TreeMap UInt64 (Std.CancellationToken × Array UInt64) compare
-- Lean.Attributes
Lean.AttributeKind.local.sizeOf_spec : sizeOf Lean.AttributeKind.local = 1
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ofExistsUnique.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F}
  (ht :
    ∀ (s : CategoryTheory.Limits.Cocone F),
      ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) l = s.ι.app j),
  CategoryTheory.Limits.IsColimit.ofExistsUnique ht =
    (fun s x => { desc := s, fac := ⋯, uniq := ⋯ }) (fun s => Classical.choose ⋯) ⋯
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.congr_symm : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_7}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (e : M ≃ₗ[R] M'),
  (LinearMap.BilinForm.congr e).symm = LinearMap.BilinForm.congr e.symm
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_binaryBicone_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y),
  P c.pt → P Y
-- Lean.Widget.InteractiveCode
Lean.Widget.SubexprInfo.mk.inj : ∀ {info : Lean.Server.WithRpcRef Lean.Elab.InfoWithCtx} {subexprPos : Lean.SubExpr.Pos}
  {diffStatus? : Option Lean.Widget.DiffTag} {info_1 : Lean.Server.WithRpcRef Lean.Elab.InfoWithCtx}
  {subexprPos_1 : Lean.SubExpr.Pos} {diffStatus?_1 : Option Lean.Widget.DiffTag},
  { info := info, subexprPos := subexprPos, diffStatus? := diffStatus? } =
      { info := info_1, subexprPos := subexprPos_1, diffStatus? := diffStatus?_1 } →
    info = info_1 ∧ subexprPos = subexprPos_1 ∧ diffStatus? = diffStatus?_1
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_inter_of_inter_eq : ∀ {α : Type u_1} (t : Set α) {s₁ s₂ s : Set α}, s₁ ∩ s = s₂ ∩ s → t.ite s₁ s₂ ∩ s = s₁ ∩ s
-- Init.Data.String.Lemmas.FindPos
String.Slice.posLT_eq_prev : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : 0 < p} (h' : String.Pos.Raw.IsValidForSlice s p),
  s.posLT p h = (s.pos p h').prev ⋯
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- The Gamma function does not vanish on `ℂ` (except at non-positive integers, where the function
is mathematically undefined and we set it to `0` by convention).  -/
Complex.Gamma_ne_zero : ∀ {s : ℂ}, (∀ (m : ℕ), s ≠ -↑m) → Complex.Gamma s ≠ 0
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
/-- If `s` is a spanning set of `Γ(X, U)`, such that each `X.basicOpen i` is affine, then `U` is also
affine.
 -/
AlgebraicGeometry.isAffineOpen_of_isAffineOpen_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (s : Set ↑(X.presheaf.obj (Opposite.op U))),
  Ideal.span s = ⊤ → (∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (X.basicOpen i)) → AlgebraicGeometry.IsAffineOpen U
-- Mathlib.RingTheory.Algebraic.Basic
/-- If `r : A` and `f : R[X]` are transcendental over `R`, then `Polynomial.aeval r f` is also
transcendental over `R`. For the converse, see `Transcendental.of_aeval` and
`transcendental_aeval_iff`.  -/
Transcendental.aeval_of_transcendental : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : A},
  Transcendental R r → ∀ {f : Polynomial R}, Transcendental R f → Transcendental R ((Polynomial.aeval r) f)