mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Syntax
/-- The implication between formulas, as a formula.  -/
FirstOrder.Language.Formula.imp : {L : FirstOrder.Language} → {α : Type u'} → L.Formula α → L.Formula α → L.Formula α
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
/-- We say that morphism `f : X ⟶ Y` is geometrically irreducible if for all `Spec K ⟶ Y` with `K`
a field, `X ×[Y] Spec K` is irreducible.  -/
AlgebraicGeometry.GeometricallyIrreducible : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Data.Complex.Basic
Complex.mk.sizeOf_spec : ∀ (re im : ℝ), sizeOf { re := re, im := im } = 1 + sizeOf re + sizeOf im
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.continuous_distDenseSeq : ∀ {X : Type u_3} [inst : MetricSpace X] [inst_1 : TopologicalSpace.SeparableSpace X] (n : ℕ),
  Continuous (Metric.PiNatEmbed.distDenseSeq X n)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelIsoOfEq_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {h : f = f},
  CategoryTheory.Limits.kernelIsoOfEq h = CategoryTheory.Iso.refl (CategoryTheory.Limits.kernel f)
-- Init.Data.String.Termination
String.Pos.eq_next_of_next?_eq_some : ∀ {s : String} {p q : s.Pos} (h : p.next? = some q), q = p.next ⋯
-- Mathlib.Order.CompactlyGenerated.Intervals
Set.Iic.isCompactElement : ∀ {α : Type u_2} [inst : CompleteLattice α] {a : α} {b : ↑(Set.Iic a)}, IsCompactElement ↑b → IsCompactElement b
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.reverse_toListRev : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toListRev.reverse = it.toList
-- Mathlib.Topology.Algebra.Group.Basic
isClosedMap_add_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (a : G),
  IsClosedMap fun x => x + a
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.comp_ite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (f : X ⟶ Y)
  (g g' : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (if P then g else g') =
    if P then CategoryTheory.CategoryStruct.comp f g else CategoryTheory.CategoryStruct.comp f g'
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.IsReduced.singleton : ∀ {α : Type u} {a : α × Bool}, FreeAddGroup.IsReduced [a]
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.neg : ∀ {𝕜 : 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 : E → F},
  Differentiable 𝕜 f → Differentiable 𝕜 (-f)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.keys_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {c : ℕ}, (Std.HashMap.Raw.emptyWithCapacity c).keys = []
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.mk_mem_interedges_comm : ∀ {α : Type u_4} {r : α → α → Prop} [inst : DecidableRel r] {s t : Finset α} {a b : α} [Std.Symm r],
  (a, b) ∈ Rel.interedges r s t ↔ (b, a) ∈ Rel.interedges r t s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InsertReplaceEdit.mk.inj : ∀ {newText : String} {insert replace : Lean.Lsp.Range} {newText_1 : String} {insert_1 replace_1 : Lean.Lsp.Range},
  { newText := newText, insert := insert, replace := replace } =
      { newText := newText_1, insert := insert_1, replace := replace_1 } →
    newText = newText_1 ∧ insert = insert_1 ∧ replace = replace_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.markTerm : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.leftShift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ γ_1 : CochainComplex.HomComplex.Cocycle K L n),
  γ = γ_1 → ∀ (a n' : ℤ) (hn' : n + a = n'), γ.leftShift a n' hn' = γ_1.leftShift a n' hn'
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.mem_innerFibrations : ∀ {X Y : SSet} (q : X ⟶ Y) [SSet.InnerFibration q], SSet.innerFibrations q
-- Lean.DocString.Types
Lean.Doc.Block.other.inj : ∀ {i : Type u} {b : Type v} {container : b} {content : Array (Lean.Doc.Block i b)} {container_1 : b}
  {content_1 : Array (Lean.Doc.Block i b)},
  Lean.Doc.Block.other container content = Lean.Doc.Block.other container_1 content_1 →
    container = container_1 ∧ content = content_1
-- Mathlib.Algebra.Order.Sub.Defs
AddLECancellable.le_tsub_of_add_le_right : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable b → a + b ≤ c → a ≤ c - b
-- Batteries.Data.List.Lemmas
List.idxOfNth_eq_idxOfNth_of_ge_countP_ge_countP : ∀ {α : Type u_1} {x : α} {n m : ℕ} [inst : BEq α] {xs : List α},
  List.count x xs ≤ n → List.count x xs ≤ m → List.idxOfNth x xs n = List.idxOfNth x xs m
-- Std.Async.Basic
/-- Obtain the `IO.TaskState` of `x`.
 -/
Std.Async.AsyncTask.getState : {α : Type} → Std.Async.AsyncTask α → BaseIO IO.TaskState
-- Std.Sat.AIG.Basic
Std.Sat.AIG.CacheHit.mk.injEq : ∀ {α : Type} {decls : Array (Std.Sat.AIG.Decl α)} {decl : Std.Sat.AIG.Decl α} (idx : ℕ) (hbound : idx < decls.size)
  (hvalid : decls[idx] = decl) (idx_1 : ℕ) (hbound_1 : idx_1 < decls.size) (hvalid_1 : decls[idx_1] = decl),
  ({ idx := idx, hbound := hbound, hvalid := hvalid } = { idx := idx_1, hbound := hbound_1, hvalid := hvalid_1 }) =
    (idx = idx_1)
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.image_list_sum : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : FunLike F α β] [inst_1 : AddMonoid α] [inst_2 : AddMonoid β]
  [AddMonoidHomClass F α β] (f : F) (l : List (Set α)), ⇑f '' l.sum = (List.map (fun s => ⇑f '' s) l).sum
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.nil_mem_paths : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X : C},
  W.paths Quiver.Path.nil
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.comp_toHom : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (hnp : L.Embedding N P) (hmn : L.Embedding M N),
  (hnp.comp hmn).toHom = hnp.toHom.comp hmn.toHom
-- Mathlib.Algebra.GroupWithZero.Regular
/-- The element `0` is regular if and only if `R` is trivial.  -/
isRegular_iff_subsingleton : ∀ {R : Type u_1} [inst : MulZeroClass R], IsRegular 0 ↔ Subsingleton R
-- Mathlib.Logic.Basic
ite_or : ∀ {α : Sort u_1} (P Q : Prop) [inst : Decidable P] (a b : α) [inst_1 : Decidable Q],
  (if P ∨ Q then a else b) = if P then a else if Q then a else b
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.map_ite_zero_one : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] {F : Type u_7}
  [inst_2 : FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) (p : Prop) [inst_4 : Decidable p],
  f (if p then 0 else 1) = if p then 0 else 1
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- A closed subgroup of a profinite group is profinite.  -/
ProfiniteGrp.ofClosedSubgroup : {G : ProfiniteGrp.{u_1}} → ClosedSubgroup ↑G.toProfinite.toTop → ProfiniteGrp.{u_1}
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
/-- **Alias** of `CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct`. -/
CategoryTheory.Functor.chosenProd.isLimit : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.CartesianMonoidalCategory C] →
      (X Y : C) →
        CategoryTheory.Limits.IsLimit
          (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)
            (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y))
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.mk.inj : ∀ {X : Type u_1} {inst : TopologicalSpace X} {k : WithTop ℕ∞} {E : Type u_2} {H : Type u_3}
  {inst_1 : NormedAddCommGroup E} {inst_2 : NormedSpace ℝ E} {inst_3 : FiniteDimensional ℝ E}
  {inst_4 : TopologicalSpace H} {I : ModelWithCorners ℝ E H} {M : Type u} {topSpaceM : TopologicalSpace M}
  {chartedSpace : ChartedSpace H M} {isManifold : IsManifold I k M} {compactSpace : CompactSpace M}
  {boundaryless : BoundarylessManifold I M} {f : M → X} {hf : Continuous f} {M_1 : Type u}
  {topSpaceM_1 : TopologicalSpace M_1} {chartedSpace_1 : ChartedSpace H M_1} {isManifold_1 : IsManifold I k M_1}
  {compactSpace_1 : CompactSpace M_1} {boundaryless_1 : BoundarylessManifold I M_1} {f_1 : M_1 → X}
  {hf_1 : Continuous f_1},
  { M := M, topSpaceM := topSpaceM, chartedSpace := chartedSpace, isManifold := isManifold,
        compactSpace := compactSpace, boundaryless := boundaryless, f := f, hf := hf } =
      { M := M_1, topSpaceM := topSpaceM_1, chartedSpace := chartedSpace_1, isManifold := isManifold_1,
        compactSpace := compactSpace_1, boundaryless := boundaryless_1, f := f_1, hf := hf_1 } →
    M = M_1 ∧ topSpaceM ≍ topSpaceM_1 ∧ chartedSpace ≍ chartedSpace_1 ∧ f ≍ f_1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x)
  [inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] [inst_8 : CompleteSpace A]
  [inst_9 : CStarRing A] (a : A) (ha : p a), (Unitization.inrNonUnitalStarAlgHom 𝕜 A).comp (cfcₙHom ha) = cfcₙAux ⋯ a ha
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.instCoeSortType : (R : Type u) → [inst : Ring R] → CoeSort (FGModuleRepr R) (Type u)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.isIntegral_algebra : ∀ (R : Type u_1) {A : Type u_2} (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [IsIntegralClosure A R B] [inst_6 : Algebra R A] [IsScalarTower R A B],
  Algebra.IsIntegral R A
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.toList_rciIter : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β}
  {t_ord : t.Ordered} {lowerBound : α},
  (Std.DTreeMap.Internal.rciIterator t lowerBound).toList =
    List.filter (fun e => (compare e.fst lowerBound).isGE) t.toList
-- Mathlib.Data.UInt
/-- To use this instance, use `open scoped USize.CommRing`.

See the module docstring for an explanation -/
USize.instCommRing : CommRing USize
-- Mathlib.Analysis.Convex.Segment
vadd_openSegment : ∀ (𝕜 : Type u_1) {E : Type u_2} {G : Type u_4} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup G] [inst_5 : Module 𝕜 E] [inst_6 : AddTorsor G E]
  [VAddCommClass G E E] (a : G) (b c : E), a +ᵥ openSegment 𝕜 b c = openSegment 𝕜 (a +ᵥ b) (a +ᵥ c)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [inst_3 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {Y X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) (f : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom ((J.plusObj P).map f.op)) (CategoryTheory.GrothendieckTopology.Plus.mk x) =
    CategoryTheory.GrothendieckTopology.Plus.mk (x.pullback f)
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.algebraMap_apply_eq_form_iff : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M] {x y : ↥(Submodule.span S (Set.range ⇑P.root))} {s : S},
  (algebraMap S R) s = (B.form ↑x) ↑y ↔ s = (B.posForm x) y
-- Mathlib.RingTheory.Valuation.Basic
Valuation.coe_ltAddSubgroup : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  (γ : Γ₀ˣ), ↑(v.ltAddSubgroup γ) = {x | v x < ↑γ}
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedNatTrans.mk.injEq : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {F G : CategoryTheory.EnrichedFunctor V C D} (out out_1 : F.forget ⟶ G.forget),
  ({ out := out } = { out := out_1 }) = (out = out_1)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.mk : ∀ {G : Type u_1} {α : Type u_2} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : autoParam (MeasureTheory.Measure α) MeasureTheory.IsFundamentalDomain._auto_1},
  MeasureTheory.NullMeasurableSet s μ →
    (∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s) →
      Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun g => g • s) → MeasureTheory.IsFundamentalDomain G s μ
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.IsLocal.of_presieve : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  {K : CategoryTheory.Precoverage C} [self : P.IsLocal K] {X : C} {R : CategoryTheory.Presieve X},
  R ∈ K.coverings X → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y) → P X
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instMulOne.eq_1 : ∀ {α : Type u_1} [inst : MulOne α],
  MulOpposite.instMulOne = { toOne := MulOpposite.instOne, toMul := MulOpposite.instMul }
-- Mathlib.Lean.Expr.Basic
/-- Returns `true` if `e` includes a `forallE` instance binder that satisfies `p`.

Cleans up annotations before traversing nested `forallE`s, and sees through `let`s.
 -/
Lean.Expr.hasInstanceBinderOf : (Lean.Expr → Bool) → Lean.Expr → Bool
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.coe_extendScalars : ∀ {L : Type u_2} [inst : Field L] {F E : Subfield L} (h : F ≤ E), ↑(Subfield.extendScalars h) = ↑E
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.fromAffine_some_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [inst_1 : Nontrivial R] {X Y : R}
  (h : W'.toAffine.Nonsingular X Y),
  WeierstrassCurve.Jacobian.Point.fromAffine (WeierstrassCurve.Affine.Point.some X Y h) ≠ 0
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.ofDual : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  BoundedVariationOn f s → BoundedVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LevelMVarErrorInfo.msgData? : Lean.Elab.Term.LevelMVarErrorInfo → Option Lean.MessageData
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.eRk X = (M.restrict X).eRank
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.biSup : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Type u_5} (s : Set ι) {f : ι → δ → α},
  s.Countable → (∀ i ∈ s, Measurable (f i)) → Measurable fun b => ⨆ i ∈ s, f i b
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_assoc : ∀ {m n : ℕ} {α : Sort u_1} {p : ℕ} (a : Fin m → α) (b : Fin n → α) (c : Fin p → α),
  Fin.append (Fin.append a b) c = Fin.append a (Fin.append b c) ∘ Fin.cast ⋯
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.enorm : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (fun x => ‖f x‖ₑ) μ
-- Mathlib.Topology.JacobsonSpace
JacobsonSpace.discreteTopology : ∀ {X : Type u_1} [inst : TopologicalSpace X] [JacobsonSpace X], (closedPoints X).Finite → DiscreteTopology X
-- Mathlib.Algebra.Group.Shrink
Shrink.instMonoid : {α : Type u_2} → [inst : Small.{v, u_2} α] → [Monoid α] → Monoid (Shrink.{v, u_2} α)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.brecOn.go : {α : Type} →
  {motive : Std.Tactic.BVDecide.BoolExpr α → Sort u} →
    (t : Std.Tactic.BVDecide.BoolExpr α) →
      ((t : Std.Tactic.BVDecide.BoolExpr α) → Std.Tactic.BVDecide.BoolExpr.below t → motive t) →
        motive t ×' Std.Tactic.BVDecide.BoolExpr.below t
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Ensure that `forget₂ AddCommMonCat AddMonCat` automatically reflects isomorphisms.  -/
AddCommMonCat.forget₂_full : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).Full
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.nontrivial_iff : ∀ {R : Type u_1} [inst : MonoidWithZero R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S],
  Nontrivial (OreLocalization S R) ↔ 0 ∉ S
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.monodromy_map : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {x y : E} (γ : Path.Homotopic.Quotient x y),
  cov.monodromy (γ.map { toFun := p, continuous_toFun := ⋯ }) ⟨x, ⋯⟩ = ⟨y, ⋯⟩
-- Mathlib.Probability.Kernel.MeasurableIntegral
MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {a : α} {E : Type u_4} [inst : NormedAddCommGroup E] {η : ProbabilityTheory.Kernel (α × β) γ}
  [ProbabilityTheory.IsSFiniteKernel η] [inst_2 : NormedSpace ℝ E] {f : β × γ → E},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ∫ (y : γ), f (x, y) ∂η (a, x)
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivative_X : ∀ {R : Type u_1} [inst : CommSemiring R], (PowerSeries.derivative R) PowerSeries.X = 1
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.lintegral_prod_id : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ENNReal},
  Measurable f →
    ∀ (κ : ProbabilityTheory.Kernel β α) [ProbabilityTheory.IsSFiniteKernel κ] (b : β),
      ∫⁻ (p : α × β), f p ∂(κ.prod ProbabilityTheory.Kernel.id) b = ∫⁻ (a : α), f (a, b) ∂κ b
-- Mathlib.Algebra.Group.Int.Defs
Int.instIsAddTorsionFree : IsAddTorsionFree ℤ
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.truncTotal_subst_eq_truncTotal_sum_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {f : MvPowerSeries σ R} [inst_3 : Finite τ] {k : ℕ},
  MvPowerSeries.HasSubst a →
    (∀ (i : σ), MvPowerSeries.constantCoeff (a i) = 0) →
      (MvPowerSeries.truncTotal k) (MvPowerSeries.subst a f) =
        (MvPowerSeries.truncTotal k)
          (∑ i ∈ Finset.range k, MvPowerSeries.subst a ((MvPowerSeries.homogeneousComponent i) f))
-- Mathlib.Topology.VectorBundle.Riemannian
/-- A fiber in a bundle satisfying the `[RiemannianBundle E]` typeclass inherits
a `NormedAddCommGroup` structure.

The normal priority for an instance which always applies like this one should be 100.
We use 80 as this is rather specialized, so we want other paths to be tried first typically.
As this instance is quite specific and very costly because of higher-order unification, we
also scope it to the `Bundle` namespace.  -/
Bundle.instNormedAddCommGroupOfRiemannianBundleOfIsTopologicalAddGroupOfContinuousConstSMulReal : {B : Type u_7} →
  {E : B → Type u_8} →
    [inst : (b : B) → TopologicalSpace (E b)] →
      [inst_1 : (b : B) → AddCommGroup (E b)] →
        [inst_2 : (b : B) → Module ℝ (E b)] →
          [h : Bundle.RiemannianBundle E] →
            [∀ (b : B), IsTopologicalAddGroup (E b)] →
              [∀ (b : B), ContinuousConstSMul ℝ (E b)] → (b : B) → NormedAddCommGroup (E b)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.type₁_d : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (hx : SSet.prodStdSimplex.pairingCore.IsType₂ x) {d : ℕ} (hd : x.dim = d), (hx.type₁ hd).d = d
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.insertMany_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {l : List α} {k : α},
  t.insertMany (k :: l) = (t.insert k).insertMany l
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The opcycles in the opposite category of the opposite of a short complex identifies
to the cycles of this short complex.  -/
CategoryTheory.ShortComplex.opcyclesOpIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasLeftHomology] → S.op.opcycles ≅ Opposite.op S.cycles
-- Mathlib.Data.Prod.Basic
Prod.snd_surjective : ∀ {α : Type u_1} {β : Type u_2} [h : Nonempty α], Function.Surjective Prod.snd
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- The image of a subcomplex by a morphism of simplicial sets.  -/
SSet.Subcomplex.image : {X Y : SSet} → X.Subcomplex → (X ⟶ Y) → Y.Subcomplex
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.t_fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i j k : self.J)
  (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
  CategoryTheory.CategoryStruct.comp (self.t' i j k hij hik hjk)
      (CategoryTheory.Limits.pullback.snd (self.f j k hjk) (self.f j i ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (self.f i j hij) (self.f i k hik))
      (self.t i j hij)
-- Mathlib.Order.Preorder.Chain
IsChain.pair : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, r a b → IsChain r {a, b}
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.commGroupWithZero : (A : Type u) →
  [inst : CommRing A] →
    (K : Type v) → [inst_1 : Field K] → [inst_2 : Algebra A K] → CommGroupWithZero (ValuationRing.ValueGroup A K)
-- Mathlib.Topology.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] (f : α → β),
  OmegaCompletePartialOrder.ωScottContinuous f = ScottContinuousOn (Set.range fun c => Set.range ⇑c) f
-- Mathlib.Tactic.FunProp.FunctionData
/-- Structure storing parts of a function in funProp-normal form.  -/
Mathlib.Meta.FunProp.FunctionData : Type
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_eq_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α} [MulLeftMono α], a⁻ᵐ = 1 ↔ 1 ≤ a
-- Mathlib.Analysis.Normed.Module.Bases
/-- Projection onto a finite set of basis vectors.  -/
GeneralSchauderBasis.proj : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} →
      [inst_1 : NormedAddCommGroup X] →
        [inst_2 : NormedSpace 𝕜 X] →
          {β : Type u_3} → {L : SummationFilter β} → GeneralSchauderBasis β 𝕜 X L → Finset β → X →L[𝕜] X