mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- The `PullbackCone` obtained by pasting two `PullbackCone`'s horizontally  -/
CategoryTheory.Limits.PullbackCone.pasteHoriz : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₃ Y₁ Y₂ Y₃ : C} →
      {g₁ : Y₁ ⟶ Y₂} →
        {g₂ : Y₂ ⟶ Y₃} →
          {i₃ : X₃ ⟶ Y₃} →
            (t₂ : CategoryTheory.Limits.PullbackCone g₂ i₃) →
              {i₂ : t₂.pt ⟶ Y₂} →
                CategoryTheory.Limits.PullbackCone g₁ i₂ →
                  i₂ = t₂.fst → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp g₁ g₂) i₃
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.lie_mem : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) {x y : L}, x ∈ L' → y ∈ L' → ⁅x, y⁆ ∈ L'
-- Lean.Meta.Basic
/-- `withImplicit x` executes `x` using the `.implicit` transparency setting. In this setting `[reducible]`,
`[instance_reducible]`, and `[implicit_reducible]` definitions are all unfolded. Used for
definitional equality checks on implicit *value* arguments, where `[implicit_reducible]` definitions
need to unfold in addition to what `.instances` already unfolds.
 -/
Lean.Meta.withImplicit : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.Topology.Compactification.StoneCech
ultrafilter_extend_pure : ∀ {α : Type u} {γ : Type u_1} [inst : TopologicalSpace γ] [T2Space γ] (f : α → γ) (a : α),
  Ultrafilter.extend f (pure a) = f a
-- Init.Prelude
Nat.lt_add_one : ∀ (n : ℕ), n < n + 1
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.center_le_centralizer : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), AddSubgroup.center G ≤ AddSubgroup.centralizer s
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.cm4b : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C] {A B X Y : C}
  (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.Fibration p]
  [HomotopicalAlgebra.WeakEquivalence p], CategoryTheory.HasLiftingProperty i p
-- Mathlib.Data.Fin.SuccPred
Fin.castLE_comp_castSucc : ∀ {n m : ℕ} (h : n + 1 ≤ m), Fin.castLE h ∘ Fin.castSucc = Fin.castLE ⋯
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_smul_of_tower : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  {p : Submodule R M} [inst_2 : SMul S R] [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (r : S) (x : ↥p),
  ↑(r • x) = r • ↑x
-- Mathlib.RingTheory.Ideal.Operations
/-- Another version of prime avoidance using `Set.Finite` instead of `Finset`.  -/
Ideal.subset_union_prime_finite : ∀ {R : Type u_2} {ι : Type u_3} [inst : CommRing R] {s : Set ι},
  s.Finite →
    ∀ {f : ι → Ideal R} (a b : ι),
      (∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime) → ∀ {I : Ideal R}, ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
-- Mathlib.Order.Filter.Pointwise
Filter.mem_add : ∀ {α : Type u_2} [inst : Add α] {f g : Filter α} {s : Set α}, s ∈ f + g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ + t₂ ⊆ s
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.hom₂_ext : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y} {η θ : f ⟶ g}, η.hom = θ.hom → η = θ
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.top_coe : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L], ↑⊤ = Set.univ
-- Mathlib.Data.Set.Finite.Basic
Finite.Set.subset : ∀ {α : Type u} (s : Set α) {t : Set α} [Finite ↑s], t ⊆ s → Finite ↑t
-- Mathlib.RingTheory.Unramified.Finite
Algebra.FormallyUnramified.elem.congr_simp : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Algebra.FormallyUnramified R S] [inst_4 : Algebra.EssFiniteType R S],
  Algebra.FormallyUnramified.elem R S = Algebra.FormallyUnramified.elem R S
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioc_pred_right_eq_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] (a b : α),
  Finset.Ioc a (Order.pred b) = Finset.Ioo a b
-- Lean.Class
/-- Switch the state into persistent mode. We switch to this mode after
we read all imported .olean files.
Recall that we use a `SMap` for implementing the state of the type class environment extension.
 -/
Lean.ClassState.switch : Lean.ClassState → Lean.ClassState
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_eq_append : ∀ {m n : ℕ}, m ≤ n → (m...=n).toList = (m...n).toList ++ [n]
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
/-- Chooses an entering variable: among the variables with a positive coefficient in the objective
function, the one with the smallest index (in the initial indexing).
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.chooseEnteringVar : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmM matType ℕ
-- Init.Data.Float.Float
/-- Converts a floating-point number to a word-sized unsigned integer.

If the given `Float` is non-negative, truncates the value to a positive integer, rounding down and
clamping to the range of `USize`. Returns `0` if the `Float` is negative or `NaN`, and returns the
largest `USize` value (i.e. `USize.size - 1`) if the float is larger than it.

This function has a logical model in terms of `Float.Model`.
 -/
Float.toUSize : Float → USize
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.inner_rightAngleRotation_left : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), inner ℝ (o.rightAngleRotation x) y = (o.areaForm x) y
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.toLin'_injective : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R],
  Function.Injective ⇑Matrix.SpecialLinearGroup.toLin'
-- Lean.HeadIndex
Lean.HeadIndex.forallE : Lean.HeadIndex
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_neg : ∀ {V W : SemiNormedGrp} (f : V ⟶ W), SemiNormedGrp.Hom.hom (-f) = -SemiNormedGrp.Hom.hom f
-- Lean.Meta.LazyDiscrTree
/-- Collect all values from a subtree recursively and clear them.  -/
Lean.Meta.LazyDiscrTree.collectSubtreeAux : {α : Type} → Lean.Meta.LazyDiscrTree.TrieIndex → Lean.Meta.LazyDiscrTree.MatchM α (Array α)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.opEquiv_functor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x : (CategoryTheory.WithInitial C)ᵒᵖ),
  (CategoryTheory.WithInitial.opEquiv C).functor.obj x =
    match Opposite.unop x with
    | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
    | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star
-- Mathlib.Order.Directed
DirectedOn.is_top_of_is_max : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → ∀ {m : α}, m ∈ s → (∀ a ∈ s, m ≤ a → a ≤ m) → ∀ a ∈ s, a ≤ m
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- A finite-dimensional subspace is closed.  -/
Submodule.closed_of_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E] [T2Space E]
  (s : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥s], IsClosed ↑s
-- Lean.Parser.Do
Lean.Parser.Term.doBreak.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- The reproducing kernel Hilbert space generated by a positive semidefinite matrix.
TODO: Make nonexposed def once deriving is fixed. See
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency/near/578850754  -/
RKHS.OfKernel : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : CompleteSpace V] →
              (K : Matrix X X (V →L[𝕜] V)) → [Fact K.PosSemidef] → Type (max (max u_3 u_2) u_1)
-- Mathlib.Order.Filter.Lift
Filter.tendsto_prod_self_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α × α → β} {x : Filter α} {y : Filter β},
  Filter.Tendsto f (x ×ˢ x) y ↔ ∀ W ∈ y, ∃ U ∈ x, ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W
-- Mathlib.Analysis.Analytic.Basic
AnalyticAt.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
  AnalyticAt 𝕜 f x → f =ᶠ[nhds x] g → AnalyticAt 𝕜 g x
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.lift'.eq_1 : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} D]
  (obj : V → D) (map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w))
  (map_id : ∀ (v : V), map (CategoryTheory.ReflQuiver.id v) = CategoryTheory.CategoryStruct.id (obj v)),
  CategoryTheory.Cat.FreeRefl.lift' obj map map_id =
    CategoryTheory.Cat.FreeRefl.lift { obj := obj, map := fun {X Y} => map, map_id := map_id }
-- Std.Time.Time.Unit.Second
Std.Time.Second.instDecidableLtOffset : {x y : Std.Time.Second.Offset} → Decidable (x < y)
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.isZero_quotient_obj_iff : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} (C : HomologicalComplex V c),
  CategoryTheory.Limits.IsZero ((HomotopyCategory.quotient V c).obj C) ↔
    Nonempty (Homotopy (CategoryTheory.CategoryStruct.id C) 0)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `Units.le_inv_mul_iff`. -/
Units.mul_le_of_le_inv_mul : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a b : M}, a ≤ ↑u⁻¹ * b → ↑u * a ≤ b
-- Mathlib.Analysis.RCLike.Basic
RCLike.abs_re_le_norm : ∀ {K : Type u_1} [inst : RCLike K] (z : K), |RCLike.re z| ≤ ‖z‖
-- Mathlib.Topology.Irreducible
Subtype.preirreducibleSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsPreirreducible s → PreirreducibleSpace ↑s
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_int64ToBitVec : ∀ (x : Int64), Int8.ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResultCore.subgoal.inj : ∀ {mvarId : Lean.MVarId} {numNewEqs : ℕ} {mvarId_1 : Lean.MVarId} {numNewEqs_1 : ℕ},
  Lean.Meta.InjectionResultCore.subgoal mvarId numNewEqs = Lean.Meta.InjectionResultCore.subgoal mvarId_1 numNewEqs_1 →
    mvarId = mvarId_1 ∧ numNewEqs = numNewEqs_1
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue!_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited γ] {f : α → β → γ}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      Std.Internal.List.getKey? k l = some k' →
        Std.Internal.List.getValue! k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) =
          (Option.map (f k') (Std.Internal.List.getValue? k l)).get!
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_of_im_neg : ∀ {z : ℂ}, z.im < 0 → z.arg = -Real.arccos (z.re / ‖z‖)
-- Mathlib.Algebra.CharP.Defs
/-- The exponential characteristic is one if the characteristic is zero.  -/
char_zero_of_expChar_one : ∀ (R : Type u_1) [inst : NonAssocSemiring R] [Nontrivial R] (p : ℕ) [hp : CharP R p] [hq : ExpChar R 1], p = 0
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear : ∀ (z : UpperHalfPlane) (a b : ℤ), Summable fun m => 1 / (↑m * ↑z + ↑a) - 1 / (↑m * ↑z + ↑b)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α},
  Std.ExtDTreeMap.Const.get? (t₁ \ t₂) k = if k ∈ t₂ then none else Std.ExtDTreeMap.Const.get? t₁ k
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.MonadCommRing.mk : {m : Type → Type} →
  m Lean.Meta.Grind.Arith.CommRing.CommRing →
    ((Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.Meta.Grind.Arith.CommRing.CommRing) → m Unit) →
      Lean.Meta.Grind.Arith.CommRing.MonadCommRing m
-- Mathlib.Geometry.Euclidean.Volume.Measure
/-- If `d₁ < d₂`, then for any set s we have either `μHE[d₂] s = 0`, or `μHE[d₁] s = ∞`.  -/
MeasureTheory.Measure.euclideanHausdorffMeasure_zero_or_top : ∀ {X : Type u_1} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d₁ d₂ : ℕ},
  d₁ < d₂ →
    ∀ (s : Set X),
      (MeasureTheory.Measure.euclideanHausdorffMeasure d₂) s = 0 ∨
        (MeasureTheory.Measure.euclideanHausdorffMeasure d₁) s = ⊤
-- Batteries.Data.List.Lemmas
List.findIdxNth_zero : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.findIdxNth p xs 0 = List.findIdx p xs
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.toArray_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  {f : α → β → Option γ},
  t.WF →
    Std.DTreeMap.Raw.Const.toArray (Std.DTreeMap.Raw.filterMap f t) =
      Array.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DTreeMap.Raw.Const.toArray t)
-- Mathlib.LinearAlgebra.DFinsupp
/-- If `DFinsupp.sumAddHom` applied with `AddSubmonoid.subtype` is injective then the additive
submonoids are independent.  -/
iSupIndep_of_dfinsuppSumAddHom_injective : ∀ {ι : Type u_1} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : AddCommMonoid N] (p : ι → AddSubmonoid N),
  Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype) → iSupIndep p
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVec.refs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {w : ℕ} → aig.RefVec w → Vector Std.Sat.AIG.Fanin w
-- Mathlib.Order.Disjoint
isCompl_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {a b : α},
  IsCompl a b ↔ Disjoint a b ∧ Codisjoint a b
-- Mathlib.Analysis.Calculus.Deriv.Basic
toSpanSingleton_derivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  ContinuousLinearMap.toSpanSingleton 𝕜 (derivWithin f s x) = fderivWithin 𝕜 f s x
-- Init.Data.List.Lemmas
List.filterMap_cons_some : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {a : α} {l : List α} {b : β},
  f a = some b → List.filterMap f (a :: l) = b :: List.filterMap f l
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.symm_apply_apply : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] (e : A ≃⋆* B)
  (x : A), e.symm (e x) = x
-- Mathlib.Data.Int.LeastGreatest
/-- If `P : ℤ → Prop` is a predicate such that the set `{m : P m}` is bounded above and nonempty,
then this set has the greatest element. This lemma uses classical logic to avoid assumption
`[DecidablePred P]`. See `Int.greatestOfBdd` for a constructive counterpart.  -/
Int.exists_greatest_of_bdd : ∀ {P : ℤ → Prop}, (∃ b, ∀ (z : ℤ), P z → z ≤ b) → (∃ z, P z) → ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.comp_f₀_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : CategoryTheory.ShortComplex C}
  (h : S₃.L₀ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).f₀ h =
    CategoryTheory.CategoryStruct.comp f.f₀ (CategoryTheory.CategoryStruct.comp g.f₀ h)
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If a function is `C^n` with `1 ≤ n`, then the derivative of `f` is also a strict derivative.  -/
ContDiff.hasStrictFDerivAt : ∀ {n : WithTop ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {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'}
  {x : E'}, ContDiff 𝕂 n f → n ≠ 0 → HasStrictFDerivAt f (fderiv 𝕂 f x) x
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.coe_zpowers : ∀ {G : Type u_1} [inst : Group G] (g : G), ↑(Subgroup.zpowers g) = Set.range fun x => g ^ x
-- Std.Data.Internal.Cut
Std.Internal.IsCut : {α : Type u} → (α → α → Ordering) → (α → Ordering) → Prop
-- Mathlib.RingTheory.Radical.Basic
/-- The finite set of prime factors of an element in a unique factorization monoid.  -/
UniqueFactorizationMonoid.primeFactors : {M : Type u_1} → [inst : CommMonoidWithZero M] → [NormalizationMonoid M] → [UniqueFactorizationMonoid M] → M → Finset M
-- Mathlib.Algebra.GCDMonoid.Basic
normUnit_coe_units : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (u : αˣ), normUnit ↑u = u⁻¹
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- the underlying topological space of `Proj` restricted to some open set  -/
_private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme.0.AlgebraicGeometry.«termProj.T|_» : Lean.ParserDescr
-- Init.Data.String.Basic
String.Slice.Pos.ofSlice_inj : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos₁ pos₂ : (s.slice p₀ p₁ h).Pos),
  String.Slice.Pos.ofSlice pos₁ = String.Slice.Pos.ofSlice pos₂ ↔ pos₁ = pos₂
-- Mathlib.Topology.Maps.Proper.Basic
IsProperMap.toContinuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f → Continuous f
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The topology of convergence in distribution on a separable space is pseudo-metrizable.  -/
MeasureTheory.instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace : ∀ (X : Type u_2) [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X]
  [TopologicalSpace.SeparableSpace X] [inst_3 : MeasurableSpace X] [inst_4 : OpensMeasurableSpace X],
  TopologicalSpace.PseudoMetrizableSpace (MeasureTheory.ProbabilityMeasure X)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.regularTopology.eq_induced : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [inst_2 : F.PreservesEffectiveEpis]
  [inst_3 : F.ReflectsEffectiveEpis] [inst_4 : F.Full] [inst_5 : F.Faithful] [inst_6 : F.EffectivelyEnough]
  [inst_7 : CategoryTheory.Preregular D],
  CategoryTheory.regularTopology C = F.inducedTopology (CategoryTheory.regularTopology D)
-- Init.Data.String.Lemmas.Splits
String.Pos.splits_toSlice_iff : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String}, p.toSlice.Splits t₁ t₂ ↔ p.Splits t₁ t₂
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.instCommMonoidWithZero : {R : Type u_1} →
  [inst : CommMonoidWithZero R] →
    {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → CommMonoidWithZero (OreLocalization S R)
-- Mathlib.RingTheory.Kaehler.Basic
Derivation.liftKaehlerDifferential_unique_iff : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  {f f' : Ω[S⁄R] →ₗ[S] M}, f = f' ↔ f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
-- Mathlib.NumberTheory.Padics.Complex
/-- The norm on `ℂ_[p]` is compatible with the valuation.  -/
PadicComplex.norm_eq_norm' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], (fun x => ‖x‖) = Valued.v.norm
-- Init.Data.List.Nat.Modify
List.getElem_modifyHead : ∀ {α : Type u_1} {l : List α} {f : α → α} {i : ℕ} (h : i < (List.modifyHead f l).length),
  (List.modifyHead f l)[i] = if h' : i = 0 then f l[0] else l[i]
-- Mathlib.Analysis.Normed.Group.Hom
/-- Given a normed group hom `f : V₁ → V₂` satisfying `g.comp f = 0` for some `g : V₂ → V₃`,
the corestriction of `f` to the kernel of `g`.  -/
NormedAddGroupHom.ker.lift : {V₁ : Type u_3} →
  {V₂ : Type u_4} →
    {V₃ : Type u_5} →
      [inst : SeminormedAddCommGroup V₁] →
        [inst_1 : SeminormedAddCommGroup V₂] →
          [inst_2 : SeminormedAddCommGroup V₃] →
            (f : NormedAddGroupHom V₁ V₂) → (g : NormedAddGroupHom V₂ V₃) → g.comp f = 0 → NormedAddGroupHom V₁ ↥g.ker
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- ```
   0 -----0---> X
   |            |
   0           inl
   |            |
   v            v
   Y --inr--> X ⊞ Y
```
is a bi-Cartesian square.
 -/
CategoryTheory.BicartesianSq.of_is_biproduct₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y}
  (h : b.IsBilimit), CategoryTheory.BicartesianSq 0 0 b.inl b.inr
-- Mathlib.Algebra.Order.Monoid.Defs
add_self_neg_iff : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a : α}, a + a < 0 ↔ a < 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.contains a = false → Std.ExtDHashMap.Const.get? m a = none
-- Init.Data.BitVec.Lemmas
BitVec.cpop_cons : ∀ {w : ℕ} {x : BitVec w} {b : Bool}, (BitVec.cons b x).cpop = ↑b.toNat + BitVec.setWidth (w + 1) x.cpop
-- Mathlib.Analysis.Complex.Basic
Complex.isClosed_range_intCast : IsClosed (Set.range Int.cast)
-- Std.Net.Addr
Std.Net.instInhabitedIPAddr : Inhabited Std.Net.IPAddr
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- **Alias** of `FractionalIdeal.coe_extendedHom_eq_span`. -/
FractionalIdeal.coe_extendedHomₐ_eq_span : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] [inst_12 : Algebra K L] [inst_13 : Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] (I : FractionalIdeal (nonZeroDivisors A) K),
  ↑((FractionalIdeal.extendedHom L B) I) = Submodule.span B (⇑(algebraMap K L) '' ↑I)
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {n : ℕ}
  {F : CategoryTheory.Functor (CategoryTheory.Discrete (Fin n)) C} {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsUniversalColimit c
-- Mathlib.Data.Int.WithZero
/-- Given a nonzero `e : ℝ≥0`, this is the map `ℤᵐ⁰ → ℝ≥0` sending `0 ↦ 0` and
`x ↦ e^(WithZero.unzero hx).toAdd` when `x ≠ 0` as a `MonoidWithZeroHom`.  -/
WithZeroMulInt.toNNReal : {e : NNReal} → e ≠ 0 → WithZero (Multiplicative ℤ) →*₀ NNReal
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.markTerm.go : Lean.Expr → Lean.Meta.Grind.ENode → ℕ → Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SolverTerms
-- Mathlib.Algebra.Order.Module.Defs
MulPosReflectLE.toSMulPosReflectLE : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [inst_2 : Preorder α] [MulPosReflectLE α], SMulPosReflectLE α α