mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mult.injEq : ∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon) (p_1 : Lean.Grind.CommRing.Power)
  (m_1 : Lean.Grind.CommRing.Mon),
  (Lean.Grind.CommRing.Mon.mult p m = Lean.Grind.CommRing.Mon.mult p_1 m_1) = (p = p_1 ∧ m = m_1)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- Linear combination representing a vector in the span of linearly independent vectors.

Given a family of linearly independent vectors, we can represent any vector in their span as
a linear combination of these vectors. These are provided by this linear map.
It is simply one direction of `LinearIndependent.linearCombinationEquiv`.  -/
LinearIndependent.repr : {ι : Type u'} →
  {R : Type u_2} →
    {M : Type u_4} →
      {v : ι → M} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] → LinearIndependent R v → ↥(Submodule.span R (Set.range v)) →ₗ[R] ι →₀ R
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Cycle.support_formPerm : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Cycle α) (h : s.Nodup),
  s.Nontrivial → (s.formPerm h).support = s.toFinset
-- Init.PropLemmas
right_iff_ite_iff : ∀ {p : Prop} [inst : Decidable p] {x y : Prop}, (y ↔ if p then x else y) ↔ p → y = x
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.z_zero_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (t : CategoryTheory.TwistShiftData C A) (a : A), t.z a 0 = 1
-- Batteries.Data.DList.Lemmas
_private.Batteries.Data.DList.Lemmas.0.Batteries.DList.push.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.DList α → α → Sort u_2) (f : List α → List α) (h : ∀ (l : List α), f l = f [] ++ l)
  (a : α)
  (h_1 :
    (f : List α → List α) → (h : ∀ (l : List α), f l = f [] ++ l) → (a : α) → motive { apply := f, invariant := h } a),
  (match { apply := f, invariant := h }, a with
    | { apply := f, invariant := h }, a => h_1 f h a) =
    h_1 f h a
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The functions satisfying `isLocallyFraction` form a subalgebra.  -/
AlgebraicGeometry.StructureSheaf.sectionsSubalgebra : {R : Type u} →
  (A : Type u) →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
            Subalgebra R ((x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations A ↑x)
-- Mathlib.RingTheory.Ideal.Cotangent
/-- The inclusion map `I ⧸ I ^ 2` to `R ⧸ I ^ 2`.  -/
Ideal.cotangentToQuotientSquare : {R : Type u} → [inst : CommRing R] → (I : Ideal R) → I.Cotangent →ₗ[R] R ⧸ I ^ 2
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryLE!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLE! k = t₂.getEntryLE! k
-- Mathlib.Topology.Connected.Clopen
/-- A closed set `s` is preconnected if and only if for every cover by two closed sets that are
disjoint, it is contained in one of the two covering sets.  -/
isPreconnected_iff_subset_of_fully_disjoint_closed : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  IsClosed s → (IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v)
-- Mathlib.LinearAlgebra.Dimension.RankNullity
Submodule.rank_quotient_add_rank : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] (N : Submodule R M), Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
/-- The homomorphism between fundamental groups induced by a continuous map.  -/
FundamentalGroup.map : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → (f : C(X, Y)) → (x : X) → FundamentalGroup X x →* FundamentalGroup Y (f x)
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.mk'_eq_zero_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  (f : S.LocalizationMap N) (m : M) (s : ↥S), f.mk' m s = 0 ↔ ∃ s, ↑s * m = 0
-- Mathlib.Order.CompleteLattice.Basic
iSup_psigma' : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_8} {κ : ι → Sort u_9} (f : (i : ι) → κ i → α),
  ⨆ i, ⨆ j, f i j = ⨆ ij, f ij.fst ij.snd
-- Init.Data.String.Iterator
String.rawEndPos.eq_1 : ∀ (s : String), s.rawEndPos = { byteIdx := s.utf8ByteSize }
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitIsoFlipCompColim_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K),
  (CategoryTheory.Limits.colimitIsoFlipCompColim F).hom.app X =
    (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F X).hom
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.ext : ∀ {C D : CategoryTheory.Cat} {x y : C.Hom D}, x.toFunctor = y.toFunctor → x = y
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Compare the values of `PolynomialLaw.toFun'` in a square diagram,
when one of the maps is a subalgebra inclusion.  -/
PolynomialLaw.toFun'_eq_of_inclusion : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {S : Type v} [inst_5 : CommSemiring S] [inst_6 : Algebra R S]
  (f : M →ₚₗ[R] N) {A : Type u} [inst_7 : CommSemiring A] [inst_8 : Algebra R A] {φ : A →ₐ[R] S}
  (p : TensorProduct R A M) {B : Type u} [inst_9 : CommSemiring B] [inst_10 : Algebra R B] (q : TensorProduct R B M)
  {ψ : B →ₐ[R] S} (h : φ.range ≤ ψ.range),
  (LinearMap.rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p =
      (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q →
    (LinearMap.rTensor N φ.toLinearMap) (f.toFun' A p) = (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' B q)
-- Mathlib.Order.Category.Frm
/-- The underlying frame.  -/
Frm.carrier : Frm → Type u_1
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.get?ₘ : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → Option β
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  ↑((algebraMap R ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) r) =
    { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm ((algebraMap R K) r)) }
-- Mathlib.FieldTheory.Relrank
Subfield.relrank.eq_1 : ∀ {E : Type v} [inst : Field E] (A B : Subfield E), A.relrank B = Module.rank ↥(A ⊓ B) ↥(Subfield.extendScalars ⋯)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.instCoeTCOfAddDistribAddActionSemiHomClassCoeAddMonoidHom.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B] {F : Type u_10}
  [inst_6 : FunLike F A B] [inst_7 : DistribMulActionSemiHomClass F (⇑φ) A B],
  DistribMulActionHom.instCoeTCOfAddDistribAddActionSemiHomClassCoeAddMonoidHom =
    { coe := DistribMulActionSemiHomClass.toDistribMulActionHom }
-- Mathlib.GroupTheory.PushoutI
/-- Every `NormalWord` is the product of an element of the base group and a word made up
of letters each of which is in the transversal. `head` is that element of the base group.  -/
Monoid.PushoutI.NormalWord.head : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} → {d : Monoid.PushoutI.NormalWord.Transversal φ} → Monoid.PushoutI.NormalWord d → H
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instInhabitedUTLocal.default : Std.Time.TimeZone.UTLocal
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.covMatrix_submatrix : ∀ {I J : Finset NNReal} (hJI : J ⊆ I),
  ((ProbabilityTheory.BrownianReal.covMatrix I).submatrix (fun i => ⟨↑i, ⋯⟩) fun i => ⟨↑i, ⋯⟩) =
    ProbabilityTheory.BrownianReal.covMatrix J
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidCloseTextDocumentParams : Type
-- Mathlib.RingTheory.Localization.Integral
/-- If `t` is `R`-integral in `S[1/r]` where `r : S` is integral over `R`,
then `r ^ n • t` is integral in `S` for some `n`.  -/
IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap : ∀ {R : Type u_5} {S : Type u_6} {Sₘ : Type u_7} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing Sₘ]
  [inst_3 : Algebra R S] [inst_4 : Algebra S Sₘ] [inst_5 : Algebra R Sₘ] [IsScalarTower R S Sₘ] {r : S},
  IsIntegral R r →
    ∀ [IsLocalization.Away r Sₘ] {x : S}, IsIntegral R ((algebraMap S Sₘ) x) → ∃ n, IsIntegral R (r ^ n * x)
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.mk.sizeOf_spec : ∀ (inner : Int16), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Order.JordanHolder
CompositionSeries.Equivalent.trans : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ s₃ : CompositionSeries X},
  s₁.Equivalent s₂ → s₂.Equivalent s₃ → s₁.Equivalent s₃
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.rfl : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f : α → β}, f ≤ᶠ[l] f
-- Mathlib.Tactic.NormNum.Basic
/-- Note: Many of the lemmas in this file use a function equality hypothesis like `f = HAdd.hAdd`
below. The reason for this is that when this is applied, to prove e.g. `100 + 200 = 300`, the
`+` here is `HAdd.hAdd` with an instance that may not be syntactically equal to the one supplied
by the `AddMonoidWithOne` instance, and rather than attempting to prove the instances equal lean
will sometimes decide to evaluate `100 + 200` directly (into whatever `+` is defined to do in this
ring), which is definitely not what we want; if the subterms are expensive to kernel-reduce then
this could cause a `(kernel) deep recursion detected` error (see https://github.com/leanprover/lean4/issues/2171, https://github.com/leanprover-community/mathlib4/pull/4048).

By using an equality for the unapplied `+` function and proving it by `rfl` we take away the
opportunity for lean to unfold the numerals (and the instance defeq problem is usually comparatively
easy).
 -/
LibraryNote.norm_num_lemma_function_equality : Batteries.Util.LibraryNote
-- Mathlib.NumberTheory.Padics.PadicNumbers
padicNormE.defn : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f : PadicSeq p) {ε : ℚ},
  0 < ε → ∃ N, ∀ i ≥ N, padicNormE (Padic.mk f - ↑(↑f i)) < ε
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.denote_toPoly : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (e : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Poly.denote ctx e.toPoly = Lean.Grind.CommRing.Expr.denote ctx e
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreCommRing.injEq : ∀ (a b : Lean.Expr) (ra rb : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly)
  (lhs' : Lean.Meta.Grind.Arith.Linear.LinExpr) (a_1 b_1 : Lean.Expr) (ra_1 rb_1 : Lean.Grind.CommRing.Expr)
  (p_1 : Lean.Grind.CommRing.Poly) (lhs'_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreCommRing a b ra rb p lhs' =
      Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreCommRing a_1 b_1 ra_1 rb_1 p_1 lhs'_1) =
    (a = a_1 ∧ b = b_1 ∧ ra = ra_1 ∧ rb = rb_1 ∧ p = p_1 ∧ lhs' = lhs'_1)
-- Mathlib.Analysis.Complex.Hadamard
/-- The supremum of the norm of `f` on imaginary lines. (Fixed real part)
This is also known as the function `M`  -/
Complex.HadamardThreeLines.sSupNormIm : {E : Type u_1} → [NormedAddCommGroup E] → (ℂ → E) → ℝ → ℝ
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mono : ∀ {R : Type u} [inst : CommSemiring R] {x y z w : R}, x ∣ y → z ∣ w → IsCoprime y w → IsCoprime x z
-- Mathlib.ModelTheory.Order
FirstOrder.Language.orderLHom_onRelation : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered] (x : ℕ) (x_1 : FirstOrder.Language.order.Relations x),
  L.orderLHom.onRelation x_1 =
    match x, x_1 with
    | .(2), FirstOrder.Language.orderRel.le => FirstOrder.Language.leSymb
-- Mathlib.Algebra.Module.Presentation.Tensor
_private.Mathlib.Algebra.Module.Presentation.Tensor.0.Module.Relations.tensor.match_1.eq_1 : ∀ {A : Type u_5} [inst : CommRing A] (relations₁ : Module.Relations A) (relations₂ : Module.Relations A)
  (motive : relations₁.R × relations₂.G ⊕ relations₁.G × relations₂.R → Sort u_6) (r₁ : relations₁.R)
  (g₂ : relations₂.G) (h_1 : (r₁ : relations₁.R) → (g₂ : relations₂.G) → motive (Sum.inl (r₁, g₂)))
  (h_2 : (g₁ : relations₁.G) → (r₂ : relations₂.R) → motive (Sum.inr (g₁, r₂))),
  (match Sum.inl (r₁, g₂) with
    | Sum.inl (r₁, g₂) => h_1 r₁ g₂
    | Sum.inr (g₁, r₂) => h_2 g₁ r₂) =
    h_1 r₁ g₂
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_comp : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R P] (f : M →ₗ[R] N)
  (g : N →ₗ[R] P), LinearMap.baseChange A (g ∘ₗ f) = LinearMap.baseChange A g ∘ₗ LinearMap.baseChange A f
-- Mathlib.Algebra.Lie.Sl2
/-- An `sl₂` triple within a Lie ring `L` is a triple of elements `h`, `e`, `f` obeying relations
which ensure that the Lie subalgebra they generate is equivalent to `sl₂`.  -/
IsSl2Triple : {L : Type u_2} → [LieRing L] → L → L → L → Prop
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_add : ∀ (a b : BitVec 32), { toBitVec := a + b } = { toBitVec := a } + { toBitVec := b }
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Given `F : WalkingParallelPair ⥤ C`, which is really the same as
`parallelPair (F.map left) (F.map right)` and a cocone on `F`, we get a cofork on
`F.map left` and `F.map right`.  -/
CategoryTheory.Limits.Cofork.ofCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} →
      CategoryTheory.Limits.Cocone F →
        CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
          (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- The functor `C ⥤ Ind C` is fully faithful.  -/
CategoryTheory.Ind.yoneda.fullyFaithful : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Ind.yoneda.FullyFaithful
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- **Alias** of `sub_apply`. -/
UniformConvergenceCLM.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.Algebra.Order.GroupWithZero.Bounds
/-- If `u v : α → β` are nonnegative and bounded above, then `u * v` is bounded above.  -/
bddAbove_range_mul : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α] {u v : α → β} [inst : Preorder β] [inst_1 : Zero β] [inst_2 : Mul β]
  [PosMulMono β] [MulPosMono β],
  BddAbove (Set.range u) → 0 ≤ u → BddAbove (Set.range v) → 0 ≤ v → BddAbove (Set.range (u * v))
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (x : ℝ),
  Measurable fun a => ↑(hf.stieltjesFunction a) x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Complex.tendsto_norm_tan_of_cos_eq_zero : ∀ {x : ℂ}, Complex.cos x = 0 → Filter.Tendsto (fun x => ‖Complex.tan x‖) (nhdsWithin x {x}ᶜ) Filter.atTop
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkGroup.fla : Std.Format.WorkGroup✝ → Std.Format.FlattenAllowability
-- Mathlib.Data.Holor
Holor.cprankMax_1 : ∀ {α : Type} {ds : List ℕ} [inst : Mul α] [inst_1 : AddMonoid α] {x : Holor α ds}, x.CPRankMax1 → Holor.CPRankMax 1 x
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.op_smul_set_mul_eq_mul_smul_set : ∀ {α : Type u_2} [inst : Semigroup α] (a : α) (s t : Set α), MulOpposite.op a • s * t = s * a • t
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.add_floor_neg_toNat_sum_eq : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] (x : ι → ℕ),
  x + ∑ i, (-IsProperLinearSet.floor✝ hs x i).toNat • ↑i =
    IsProperLinearSet.fract✝ hs x + ∑ i, (IsProperLinearSet.floor✝ hs x i).toNat • ↑i
-- Mathlib.Topology.Separation.Basic
/-- [Stacks Tag 0B31](https://stacks.math.columbia.edu/tag/0B31) (part 1) -/
Subtype.t0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {p : X → Prop}, T0Space (Subtype p)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cycles₁IsoOfIsTrivial.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  groupHomology.cycles₁IsoOfIsTrivial A = (LinearEquiv.ofTop (groupHomology.cycles₁ A) ⋯).toModuleIso
-- Mathlib.CategoryTheory.Filtered.Connected
CategoryTheory.IsFiltered.isConnected : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C], CategoryTheory.IsConnected C
-- Mathlib.Order.Hom.WithTopBot
InfHom.withBot_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (f : InfHom α β) (a : WithBot α),
  f.withBot a = WithBot.map (⇑f) a
-- Mathlib.Topology.AlexandrovDiscrete
isClopen_iInter : ∀ {ι : Sort u_1} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {f : ι → Set α},
  (∀ (i : ι), IsClopen (f i)) → IsClopen (⋂ i, f i)
-- Init.Data.BitVec.Lemmas
BitVec.mul_succ : ∀ {w : ℕ} {x y : BitVec w}, x * (y + 1#w) = x * y + x
-- Mathlib.Algebra.Order.Field.Basic
two_mul_le_add_mul_sq : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b ε : α},
  0 < ε → 2 * a * b ≤ ε * a ^ 2 + ε⁻¹ * b ^ 2
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Around a point in the target, the neighborhoods are the same within `(extChartAt I x).target`
and within `range I`.  -/
nhdsWithin_extChartAt_target_eq_of_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x : M} {z : E},
  z ∈ (extChartAt I x).target → nhdsWithin z (extChartAt I x).target = nhdsWithin z (Set.range ↑I)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.instInhabitedSelf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.Mono f] →
          Inhabited (CategoryTheory.Limits.IsImage (CategoryTheory.Limits.MonoFactorisation.self f))
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ComputedFieldView.mk.injEq : ∀ (ref modifiers : Lean.Syntax) (fieldId : Lean.Name) (type : Lean.Term)
  (matchAlts : Lean.TSyntax `Lean.Parser.Term.matchAlts) (ref_1 modifiers_1 : Lean.Syntax) (fieldId_1 : Lean.Name)
  (type_1 : Lean.Term) (matchAlts_1 : Lean.TSyntax `Lean.Parser.Term.matchAlts),
  ({ ref := ref, modifiers := modifiers, fieldId := fieldId, type := type, matchAlts := matchAlts } =
      { ref := ref_1, modifiers := modifiers_1, fieldId := fieldId_1, type := type_1, matchAlts := matchAlts_1 }) =
    (ref = ref_1 ∧ modifiers = modifiers_1 ∧ fieldId = fieldId_1 ∧ type = type_1 ∧ matchAlts = matchAlts_1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.getValue? k (Std.Internal.List.insertList l toInsert) =
        (Std.Internal.List.getValue? k toInsert).or (Std.Internal.List.getValue? k l)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.insert_sdiff_subset`. -/
Set.insert_diff_subset : ∀ {α : Type u_1} {s t : Set α} {a : α}, insert a s \ t ⊆ insert a (s \ t)
-- Mathlib.RingTheory.Norm.Defs
/-- The norm of an element `s` of an `R`-algebra is the determinant of `(*) s`.  -/
Algebra.norm : (R : Type u_1) → {S : Type u_2} → [inst : CommRing R] → [inst_1 : Ring S] → [Algebra R S] → S →* R
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If a function has a Taylor series at order at least 1, then at points in the interior of the
domain of definition, the term of order 1 of this series is a strict derivative of `f`.  -/
HasFTaylorSeriesUpToOn.hasStrictFDerivAt : ∀ {𝕂 : 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'] {n : WithTop ℕ∞} {s : Set E'}
  {f : E' → F'} {x : E'} {p : E' → FormalMultilinearSeries 𝕂 E' F'},
  HasFTaylorSeriesUpToOn n f p s →
    n ≠ 0 → s ∈ nhds x → HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕂 E' F') (p x 1)) x
-- Mathlib.Algebra.Order.Hom.Basic
/-- `MulRingSeminormClass F α` states that `F` is a type of `β`-valued multiplicative seminorms
on the ring `α`.

You should extend this class when you extend `MulRingSeminorm`.  -/
MulRingSeminormClass : (F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [NonAssocRing α] → [Semiring β] → [PartialOrder β] → [FunLike F α β] → Prop
-- Mathlib.LinearAlgebra.Multilinear.Finsupp
LinearEquiv.multilinearMapCongrRight.congr_simp : ∀ {R : Type uR} (S : Type uS) {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂]
  [inst_8 : AddCommMonoid M₃] [inst_9 : Module S M₃] [inst_10 : Module R M₃] [inst_11 : SMulCommClass R S M₃]
  [inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R] [inst_13 : LinearMap.CompatibleSMul M₃ M₂ S R] (g g_1 : M₂ ≃ₗ[R] M₃),
  g = g_1 → LinearEquiv.multilinearMapCongrRight S g = LinearEquiv.multilinearMapCongrRight S g_1
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorUnit_rel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Dial C)).rel = ⊤
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.primeCounting_sub_theta_div_log_isBigO : (fun x => ↑⌊x⌋₊.primeCounting - Chebyshev.theta x / Real.log x) =O[Filter.atTop] fun x => x / Real.log x ^ 2
-- Mathlib.Data.DFinsupp.BigOperators
/-- The `DFinsupp` version of `Finsupp.liftAddHom_apply_single`  -/
DFinsupp.liftAddHom_apply_single : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι) (x : β i),
  ((DFinsupp.liftAddHom f) fun₀ | i => x) = (f i) x
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeGPFree_smul_set₀ : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [IsCancelMulZero α] [NoZeroDivisors α] {s : Set α} {a : α},
  a ≠ 0 → (ThreeGPFree (a • s) ↔ ThreeGPFree s)