mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
/-- The **increment partition** in Szemerédi's Regularity Lemma.

If an equipartition is *not* uniform, then the increment partition is a (much bigger) equipartition
with a slightly higher energy. This is helpful since the energy is bounded by a constant (see
`Finpartition.energy_le_one`), so this process eventually terminates and yields a
not-too-big uniform equipartition.  -/
SzemerediRegularity.increment : {α : Type u_1} →
  [inst : Fintype α] →
    [inst_1 : DecidableEq α] →
      {P : Finpartition Finset.univ} →
        P.IsEquipartition → (G : SimpleGraph α) → [DecidableRel G.Adj] → ℝ → Finpartition Finset.univ
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.op_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.op.X₃ = Opposite.op S.X₁
-- Mathlib.Logic.Function.Basic
Function.pred_update : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (P : ⦃a : α⦄ → β a → Prop) (f : (a : α) → β a) (a' : α)
  (v : β a') (a : α), P (Function.update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)
-- Mathlib.Data.Multiset.Range
Multiset.range_succ : ∀ (n : ℕ), Multiset.range n.succ = n ::ₘ Multiset.range n
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.decidableMemCenter : {M : Type u_1} →
  [inst : Monoid M] → (a : M) → [Decidable (∀ (b : M), b * a = a * b)] → Decidable (a ∈ Submonoid.center M)
-- Lean.Meta.Tactic.SolveByElim
/-- Try proving the goal via `exfalso` if `solve_by_elim` otherwise fails.
This is only used when operating on a single goal.  -/
Lean.Meta.SolveByElim.ApplyRulesConfig.exfalso : Lean.Meta.SolveByElim.ApplyRulesConfig → Bool
-- Mathlib.Tactic.Linter.DirectoryDependency
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.NamePrefixRel.instEmptyCollectionNamePrefixRel : EmptyCollection Mathlib.Linter.DirectoryDependency.NamePrefixRel✝
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.IsFinite.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  {G : CategoryTheory.Subfunctor F}, (∃ ι, ∃ (_ : Finite ι), ∃ X x, Nonempty (G.IsGeneratedBy x)) → G.IsFinite
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.hasFiniteProducts_of_additive_of_essSurj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.HasFiniteProducts C] [F.Additive] [F.EssSurj], CategoryTheory.Limits.HasFiniteProducts D
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Real.cosh_eq_tsum : ∀ (r : ℝ), Real.cosh r = ∑' (n : ℕ), r ^ (2 * n) / ↑(2 * n).factorial
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.rotate_rotate : ∀ {G : Type u_2} [inst : Group G] {n : ℕ} (v : ↑(Equiv.Perm.vectorsProdEqOne G n)) (j k : ℕ),
  Equiv.Perm.VectorsProdEqOne.rotate (Equiv.Perm.VectorsProdEqOne.rotate v j) k =
    Equiv.Perm.VectorsProdEqOne.rotate v (j + k)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.getₘ_eq_getValue : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α fun x => β} (h : Std.Internal.List.containsKey k t.toListModel = true)
  {h' : (Std.DTreeMap.Internal.Impl.Const.get?ₘ t k).isSome = true},
  t.Ordered → Std.DTreeMap.Internal.Impl.Const.getₘ t k h' = Std.Internal.List.getValue k t.toListModel h
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.posLE_offset : ∀ {s : String.Slice} {p : s.Pos}, s.posLE p.offset = p
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.mul_eq_opow_log_succ : ∀ {a b : Ordinal.{u}},
  a ≠ 0 → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) b → 2 < b → a * b = b ^ Order.succ (Ordinal.log b a)
-- Init.Data.Rat.Basic
Rat.instMul : Mul ℚ
-- Mathlib.Analysis.Complex.Norm
Complex.nnnorm_I : ‖Complex.I‖₊ = 1
-- Mathlib.Algebra.Homology.QuasiIso
quasiIso_iff_comp_left : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L)
  (φ' : L ⟶ M) [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i]
  [inst_4 : ∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ],
  QuasiIso (CategoryTheory.CategoryStruct.comp φ φ') ↔ QuasiIso φ'
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.comap_inv_atTop : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G],
  Filter.comap Inv.inv Filter.atTop = Filter.atBot
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for the signed modulo operation on `BitVec`s.  -/
BitVec.reduceSMod : Lean.Meta.Simp.DSimproc
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_D' : ∀ (n : ℕ+), ADEInequality.Admissible (ADEInequality.D' n)
-- Lean.Util.MonadCache
Lean.MonadHashMapCacheAdapter.findCached? : {α β : Type} →
  {m : Type → Type} →
    [inst : BEq α] → [inst_1 : Hashable α] → [Monad m] → [Lean.MonadHashMapCacheAdapter α β m] → α → m (Option β)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.continuousOn : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {s : Set P}, ContinuousOn (⇑e) s
-- ProofWidgets.Util
_private.ProofWidgets.Util.0.Lean.PrettyPrinter.Delaborator.delabListLiteral.go : {α : Type} → Lean.PrettyPrinter.Delaborator.DelabM α → Array α → Lean.PrettyPrinter.Delaborator.DelabM (Array α)
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- The composition of two strong monomorphisms is a strong monomorphism.  -/
CategoryTheory.strongMono_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q R : C} (f : Q ⟶ P) (g : R ⟶ Q)
  [CategoryTheory.StrongMono f] [CategoryTheory.StrongMono g],
  CategoryTheory.StrongMono (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.iso_mapPullbackAdj_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (U : CategoryTheory.Over X),
  (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f.hom).counit.app U =
    CategoryTheory.Over.homMk
      (CategoryTheory.CategoryStruct.id
        (({ obj := fun Z => CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp Z.hom f.inv),
                    map := fun {Y_1 Z} g => CategoryTheory.Over.homMk (CategoryTheory.Over.Hom.left g) ⋯, map_id := ⋯,
                    map_comp := ⋯ }.comp
                (CategoryTheory.Over.map f.hom)).obj
            U).left)
      ⋯
-- Mathlib.LinearAlgebra.Projection
/-- The linear projection onto a subspace along its complement
as a map from the full space to itself, as opposed to `Submodule.projectionOnto`,
which maps into the subtype.
This version is important as it satisfies `IsIdempotentElem`.

See also:
* `Submodule.projectionOntoL` and `Submodule.projectionL` for the continuous versions.
* `Submodule.orthogonalProjection` and `Submodule.orthogonalProjectionOnto` for the projections
  along the orthogonal subspace.  -/
Submodule.projection : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} → [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → (p q : Submodule R E) → IsCompl p q → E →ₗ[R] E
-- Mathlib.Probability.Kernel.Composition.CompMap
ProbabilityTheory.Kernel.deterministic_comp_eq_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : β → γ} (hf : Measurable f) (κ : ProbabilityTheory.Kernel α β),
  (ProbabilityTheory.Kernel.deterministic f hf).comp κ = κ.map f
-- Mathlib.Geometry.Euclidean.Triangle
/-- The sum of the angles of a possibly degenerate triangle (where one of the
two given sides is nonzero), vector angle form.  -/
InnerProductGeometry.angle_add_angle_sub_add_angle_sub_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x : V) {y : V},
  y ≠ 0 →
    InnerProductGeometry.angle x y + InnerProductGeometry.angle x (x - y) + InnerProductGeometry.angle y (y - x) =
      Real.pi
-- Lean.Attributes
Lean.AttributeApplicationTime.afterCompilation : Lean.AttributeApplicationTime
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.instPartialOrder : {X : Type u_1} → PartialOrder (DiffeologicalSpace X)
-- Mathlib.Data.Set.Prod
Set.prod_self_subset_prod_self : ∀ {α : Type u_1} {s₁ s₂ : Set α}, s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂ ↔ s₁ ⊆ s₂
-- Mathlib.Data.Nat.PrimeFin
Nat.prime_of_mem_primeFactors : ∀ {n p : ℕ}, p ∈ n.primeFactors → Nat.Prime p
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] {p : Polynomial R},
  p.Monic → p.natDegree = 2 → (¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map_hom_top : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), SimpleGraph.Subgraph.map G'.hom ⊤ = G'
-- Mathlib.Tactic.Ring.Basic
/-- Applies `Int.cast` to an int polynomial to produce a polynomial in `α`.

* An atom `e` causes `↑e` to be allocated as a new atom.
* A sum delegates to `ExSum.evalIntCast`.
 -/
Mathlib.Tactic.Ring.ExBase.evalIntCast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {v : Lean.Level} →
        {β : Q(Type v)} →
          (sβ : Q(CommSemiring «$β»)) →
            {a : Q(ℤ)} →
              (rα : Q(CommRing «$α»)) →
                Mathlib.Tactic.Ring.ExBase sβ a →
                  Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.ExBase sα) q(↑«$a»))
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- Averaging with respect to a finite measure is the same as integrating against
`MeasureTheory.FiniteMeasure.normalize`.  -/
MeasureTheory.FiniteMeasure.average_eq_integral_normalize : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω) {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E],
  μ ≠ 0 → ∀ (f : Ω → E), MeasureTheory.average (↑μ) f = ∫ (ω : Ω), f ω ∂↑μ.normalize
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) {A : Type u_1}
  [inst_5 : AddCommGroup A] [inst_6 : Module ℝ A] (φ : ι → M → A),
  ∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ • φ i x₀ = ∑ᶠ (i : ι), (ρ i) x₀ • φ i x₀
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.Hom.mk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {P Q : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} →
          (app : (X : C) → (Y : D) → P.obj X Y ⟶ Q.obj X Y) →
            autoParam
                (∀ ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X') (g : Y ⟶ Y'),
                  CategoryTheory.CategoryStruct.comp (P.map f g) (app X' Y) =
                    CategoryTheory.CategoryStruct.comp (app X Y') (Q.map f g))
                CategoryTheory.ProfunctorCore.Hom.naturality._autoParam →
              P.Hom Q
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.HD_lipschitz_aux3 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty X] [Nonempty Y]
  (f g : GromovHausdorff.Cb✝ X Y), GromovHausdorff.HD f ≤ GromovHausdorff.HD g + dist f g
-- Mathlib.Order.SymmDiff
Codisjoint.bihimp_inf_bihimp_le_left : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b c : α}, Codisjoint a b → bihimp a c ⊓ bihimp b c ≤ c
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.Represents.congr_fun : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι] {A : Matrix ι ι R} {f : Module.End R M},
  Matrix.Represents b A f →
    ∀ (x : ι → R), (Fintype.linearCombination R b) (A.mulVec x) = f ((Fintype.linearCombination R b) x)
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleω₁δ a b c hab hbc).map φ).hom₁ = (t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map φ)
-- Mathlib.Logic.Equiv.Defs
/-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`.  -/
Quot.congr : {α : Sort u} →
  {β : Sort v} →
    {ra : α → α → Prop} →
      {rb : β → β → Prop} → (e : α ≃ β) → (∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)) → Quot ra ≃ Quot rb
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityISizeHOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- `n + 1` points are affinely independent if and only if their
`vectorSpan` has dimension at least `n`.  -/
affineIndependent_iff_le_finrank_vectorSpan : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] (p : ι → P) {n : ℕ},
  Fintype.card ι = n + 1 → (AffineIndependent k p ↔ n ≤ Module.finrank k ↥(vectorSpan k (Set.range p)))
-- Mathlib.Order.Interval.Set.Disjoint
IsLUB.biUnion_Iic_eq_Iio : ∀ {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α}, IsLUB s a → a ∉ s → ⋃ x ∈ s, Set.Iic x = Set.Iio a
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Result.mk.inj : ∀ {allConsts unfoldCandidates eqnCandidates : Lean.Meta.Try.Collector.OrdSet Lean.Name}
  {funIndCandidates : Lean.Meta.FunInd.SeenCalls} {indCandidates : Array Lean.Meta.Try.Collector.InductionCandidate}
  {libSearchResults : Lean.Meta.Try.Collector.OrdSet (Lean.Name × Lean.Meta.Grind.EMatchTheoremKind)}
  {allConsts_1 unfoldCandidates_1 eqnCandidates_1 : Lean.Meta.Try.Collector.OrdSet Lean.Name}
  {funIndCandidates_1 : Lean.Meta.FunInd.SeenCalls} {indCandidates_1 : Array Lean.Meta.Try.Collector.InductionCandidate}
  {libSearchResults_1 : Lean.Meta.Try.Collector.OrdSet (Lean.Name × Lean.Meta.Grind.EMatchTheoremKind)},
  { allConsts := allConsts, unfoldCandidates := unfoldCandidates, eqnCandidates := eqnCandidates,
        funIndCandidates := funIndCandidates, indCandidates := indCandidates, libSearchResults := libSearchResults } =
      { allConsts := allConsts_1, unfoldCandidates := unfoldCandidates_1, eqnCandidates := eqnCandidates_1,
        funIndCandidates := funIndCandidates_1, indCandidates := indCandidates_1,
        libSearchResults := libSearchResults_1 } →
    allConsts = allConsts_1 ∧
      unfoldCandidates = unfoldCandidates_1 ∧
        eqnCandidates = eqnCandidates_1 ∧
          funIndCandidates = funIndCandidates_1 ∧
            indCandidates = indCandidates_1 ∧ libSearchResults = libSearchResults_1
-- Mathlib.Order.Lattice
ofDual_min : ∀ {α : Type u} [inst : LinearOrder α] (a b : αᵒᵈ),
  OrderDual.ofDual (min a b) = max (OrderDual.ofDual a) (OrderDual.ofDual b)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countableOrCountablyGenerated_prod_left_swap : ∀ {β : Type u_2} {α : Type u_3} {γ : Type u_4} [inst : MeasurableSpace γ]
  [h : MeasurableSpace.CountableOrCountablyGenerated (α × β) γ], MeasurableSpace.CountableOrCountablyGenerated (β × α) γ
-- Mathlib.CategoryTheory.Idempotents.Basic
/-- If `C` and `D` are equivalent categories, that `C` is idempotent complete iff `D` is.  -/
CategoryTheory.Idempotents.isIdempotentComplete_iff_of_equivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (ε : C ≌ D),
  CategoryTheory.IsIdempotentComplete C ↔ CategoryTheory.IsIdempotentComplete D
-- Mathlib.Analysis.Normed.Group.Ultra
/-- All triangles are isosceles in an ultrametric normed group.  -/
IsUltrametricDist.norm_mul_eq_max_of_norm_ne_norm : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] {x y : S}, ‖x‖ ≠ ‖y‖ → ‖x * y‖ = max ‖x‖ ‖y‖
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.opensCone_pt : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (i : I) (U : (D.obj i).Opens),
  (AlgebraicGeometry.opensCone D c i U).pt = ↑((TopologicalSpace.Opens.map (c.π.app i).base).obj U)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokenType : Lean.ToJson Lean.Lsp.SemanticTokenType
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
instFiniteMonoidHomUnitsOfHasEnoughRootsOfUnityExponent : ∀ {G : Type u_1} {M : Type u_2} [inst : Group G] [Finite G] [inst_2 : CommMonoid M]
  [HasEnoughRootsOfUnity M (Monoid.exponent G)], Finite (G →* Mˣ)
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- a choice of a right adjoint to `L`  -/
CategoryTheory.Coreflective.R : {C : Type u₁} →
  {D : Type u₂} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        (L : CategoryTheory.Functor C D) → [self : CategoryTheory.Coreflective L] → CategoryTheory.Functor D C
-- Mathlib.Topology.Order.IsLUB
IsLUB.frequently_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsLUB s a → s.Nonempty → ∃ᶠ (x : α) in nhdsWithin a (Set.Iic a), x ∈ s
-- Mathlib.Order.Interval.Basic
Interval.dual_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (s : Interval α),
  Interval.dual (Interval.map f s) = Interval.map (OrderHom.dual f) (Interval.dual s)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, ∫⁻ (x : α), 0 ∂μ = 0
-- Init.Data.Array.Lemmas
Array.exists_of_mem_flatten : ∀ {α : Type u_1} {xss : Array (Array α)} {x : α}, x ∈ xss.flatten → ∃ xs ∈ xss, x ∈ xs
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instModulePreLp : {𝕜 : Type u_1} →
  {α : Type u_3} →
    {E : α → Type u_4} →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [inst_1 : NormedRing 𝕜] → [(i : α) → Module 𝕜 (E i)] → Module 𝕜 (PreLp E)
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.equivFinsuppOfBasisRight_apply_tmul : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq κ]
  (𝒞 : Module.Basis κ R N) (m : M) (n : N),
  (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun x => x • m) ⋯ (𝒞.repr n)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.volume_subtype_coe_eq_zero_of_volume_eq_zero : ∀ {δ : Type u_4} {u : Set δ} [inst : MeasureTheory.MeasureSpace δ],
  MeasureTheory.NullMeasurableSet u MeasureTheory.volume →
    ∀ {t : Set ↑u}, MeasureTheory.volume t = 0 → MeasureTheory.volume (Subtype.val '' t) = 0
-- Init.Data.UInt.Lemmas
UInt64.mod_one : ∀ {a : UInt64}, a % 1 = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_minKey!_eq_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.minKey! ∈ t}, t.getKey t.minKey! hc = t.minKey ⋯
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.inf_toSubfield : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (S T : IntermediateField F E), (S ⊓ T).toSubfield = S.toSubfield ⊓ T.toSubfield
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.homeomorph_symm_coe : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  [inst_1 : Topology.IsGeneratedBy X Y],
  ⇑Topology.IsGeneratedBy.homeomorph.symm = ⇑Topology.WithGeneratedByTopology.equiv.symm
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.lineDerivOp_eq_lineDerivCLM : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F] {v : E}
  {f : TestFunction Ω F ⊤}, LineDeriv.lineDerivOp v f = (TestFunction.lineDerivCLM 𝕜 v) f
-- Lean.Parser.Attr
Lean.Parser.Attr.tactic_alt.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.mulLeftReflectLE : ∀ {α : Type u} [inst : LE α] [inst_1 : Mul α] [MulLeftReflectLE α], MulLeftReflectLE αᵒᵈ
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- If `sᶜ ∉ f ↔ s ∈ f`, then `f` is an ultrafilter. The other implication is given by
`Ultrafilter.compl_notMem_iff`.  -/
Ultrafilter.ofComplNotMemIff : {α : Type u} → (f : Filter α) → (∀ (s : Set α), sᶜ ∉ f ↔ s ∈ f) → Ultrafilter α
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.image_source_inter_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (s : Set X), ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_singleton : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {a : α}, {a}.gcd = normalize a
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
SSet.Subcomplex.PairingCore.isRegular_iff_nonempty_rankFunction : ∀ {X : SSet} {A : X.Subcomplex} (P : A.PairingCore) [P.IsProper], P.IsRegular ↔ Nonempty (P.RankFunction ℕ)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.computedFields : Lean.Elab.Command.InductiveView → Array Lean.Elab.Command.ComputedFieldView
-- Mathlib.Analysis.InnerProductSpace.PiL2
Complex.orthonormalBasisOneI_repr_apply : ∀ (z : ℂ), (Complex.orthonormalBasisOneI.repr z).ofLp = ![z.re, z.im]
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If `f` is locally integrable and `g` is continuous with compact support,
then `f • g` is integrable.  -/
MeasureTheory.LocallyIntegrable.integrable_smul_right_of_hasCompactSupport : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {𝕜 : Type u_9} [inst_3 : NormedRing 𝕜] [inst_4 : Module 𝕜 E] [IsBoundedSMul 𝕜 E]
  [OpensMeasurableSpace X] [T2Space X] {f : X → 𝕜},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ {g : X → E}, Continuous g → HasCompactSupport g → MeasureTheory.Integrable (fun x => f x • g x) μ
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.Subcomplex.eq_top_iff_contains_nonDegenerate : ∀ {X : SSet} (A : X.Subcomplex), A = ⊤ ↔ ∀ (n : ℕ), X.nonDegenerate n ⊆ A.obj (Opposite.op { len := n })
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.toList_toTake : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toTake.toList = it.toList