mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl_comp_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f),
  (MvPolynomial.killCompl hf).comp (MvPolynomial.rename f) = AlgHom.id R (MvPolynomial σ R)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Grp.instCategory =
    { Hom := CategoryTheory.Grp.instCategory._aux_1, id := CategoryTheory.Grp.instCategory._aux_3,
      comp := @CategoryTheory.Grp.instCategory._aux_5 C inst inst_1, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.abs_sum_le_sum_abs : ∀ {ι : Type u_1} {G : Type u_9} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (f : ι → G)
  (s : Finset ι), |∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i|
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.isSpanning_iff : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G'.IsSpanning ↔ G'.verts = Set.univ
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.mergeSort.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (a : α) (x : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match [a], x with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_2 a x
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT.congr_simp : ∀ (n n_1 : ℕ) (e_n : n = n_1) (h : n < UInt32.size), UInt32.ofNatLT n h = UInt32.ofNatLT n_1 ⋯
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitKind : Type
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.spanCoeffs.eq_1 : ∀ (k : Type u) [inst : Field k],
  AlgebraicClosure.spanCoeffs k = Ideal.span (Set.range fun fn => (AlgebraicClosure.subProdXSubC fn.1).coeff fn.2)
-- Init.Data.Dyadic.Basic
Dyadic.instLawfulOrderLT : Std.LawfulOrderLT Dyadic
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableWithinAt_natCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {x : E} {s : Set E} [inst_7 : NatCast F] (n : ℕ), DifferentiableWithinAt 𝕜 (↑n) s x
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The cofan `s.cofan Δ` is colimit.  -/
CategoryTheory.SimplicialObject.Splitting.isColimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) → (Δ : SimplexCategoryᵒᵖ) → CategoryTheory.Limits.IsColimit (s.cofan Δ)
-- Init.Prelude
/-- The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. -/
Prod : Type u → Type v → Type (max u v)
-- Mathlib.Data.ZMod.QuotientGroup
/-- The quotient `(a ^ ℤ) ⧸ (stabilizer b)` is cyclic of order `minimalPeriod ((•) a) b`.  -/
MulAction.zpowersQuotientStabilizerEquiv : {α : Type u_3} →
  {β : Type u_4} →
    [inst : Group α] →
      (a : α) →
        [inst_1 : MulAction α β] →
          (b : β) →
            ↥(Subgroup.zpowers a) ⧸ MulAction.stabilizer (↥(Subgroup.zpowers a)) b ≃*
              Multiplicative (ZMod (Function.minimalPeriod (fun x => a • x) b))
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.getDoSeqElems : Lean.Syntax → List Lean.Syntax
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Range : Type
-- Init.Data.Vector.Lemmas
Vector.toList_take : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, (xs.take i).toList = List.take i xs.toList
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.cokernelSolution_var : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (g : (pres₂.cokernelRelations data).G),
  (pres₂.cokernelSolution data).var g = f.range.mkQ (pres₂.var g)
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Context : Type
-- Init.Data.Fin.Basic
Fin.instDiv : {n : ℕ} → Div (Fin n)
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- A natural transformation of functors F ⟶ F' induces a map end_ F ⟶ end_ F'.  -/
CategoryTheory.Limits.end_.map : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          [inst_2 : CategoryTheory.Limits.HasEnd F] →
            {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
              [inst_3 : CategoryTheory.Limits.HasEnd F'] →
                (F ⟶ F') → (CategoryTheory.Limits.end_ F ⟶ CategoryTheory.Limits.end_ F')
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.map_exp_atTop : Filter.map Real.exp Filter.atTop = Filter.atTop
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
/-- Alternate version of `Real.multipliable_of_summable_log` assuming only that positivity holds
eventually.  -/
Real.multipliable_of_summable_log' : ∀ {ι : Type u_1} {f : ι → ℝ},
  (∀ᶠ (i : ι) in Filter.cofinite, 0 < f i) → (Summable fun i => Real.log (f i)) → Multipliable f
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.extend.congr_simp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6}
  [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜₂] [inst_2 : AddCommGroup E]
  [inst_3 : NormedAddCommGroup Eₗ] [inst_4 : AddCommGroup F] [inst_5 : NormedAddCommGroup Fₗ] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 Eₗ] [inst_8 : IsBoundedSMul 𝕜 Eₗ] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₂ Fₗ]
  [inst_11 : IsBoundedSMul 𝕜₂ Fₗ] [inst_12 : CompleteSpace Eₗ] [inst_13 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_14 : RingHomInvPair σ₁₂ σ₂₁] [inst_15 : RingHomInvPair σ₂₁ σ₁₂] (f f_1 : E ≃ₛₗ[σ₁₂] F)
  (e_f : f = f_1) (e₁ e₁_1 : E →ₗ[𝕜] Eₗ) (e_e₁ : e₁ = e₁_1) (e₂ e₂_1 : F →ₗ[𝕜₂] Fₗ) (e_e₂ : e₂ = e₂_1)
  (h_dense₁ : DenseRange ⇑e₁) (h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖) (h_dense₂ : DenseRange ⇑e₂)
  (h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖),
  f.extend e₁ e₂ h_dense₁ h_norm₁ h_dense₂ h_norm₂ = f_1.extend e₁_1 e₂_1 ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- A point in `K` with the orthogonality property (here characterized in terms of `Kᗮ`) must be the
orthogonal projection.  -/
Submodule.eq_starProjection_of_mem_orthogonal' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {u v z : E},
  v ∈ K → z ∈ Kᗮ → u = v + z → K.starProjection u = v
-- Init.Conv
/-- A list `1 2 4` of occurrences means to apply to the first, second, and fourth
occurrence of the pattern.
 -/
Lean.Parser.Tactic.Conv.occsIndexed : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.apply_one : ∀ {R : Type u_1} [inst : NonUnitalRing R] [inst_1 : DecidableEq R] (x : R), 1 x = if x = 0 then 0 else 1
-- Mathlib.RingTheory.OreLocalization.Basic
/-- `zsmul` of `OreLocalization`  -/
OreLocalization.zsmul : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddGroup X] → [inst_3 : DistribMulAction R X] → ℤ → OreLocalization S X → OreLocalization S X
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActivateNextGuardResult.next : Lean.Expr → List Lean.Meta.Grind.TheoremGuard → Lean.Meta.Grind.ActivateNextGuardResult
-- Lean.Elab.Arg
Lean.Elab.Term.instToMessageDataNamedArg : Lean.ToMessageData Lean.Elab.Term.NamedArg
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.addBottom_map : ∀ {K : Type u_1} {Γ : K → Type u_2} (L : Turing.ListBlank ((k : K) → Option (Γ k))),
  Turing.ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (Turing.TM2to1.addBottom L) = L
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.node.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : α) (child sibling : Batteries.PairingHeapImp.Heap α),
  sizeOf (Batteries.PairingHeapImp.Heap.node a child sibling) = 1 + sizeOf a + sizeOf child + sizeOf sibling
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitConeLeftOpOfCocone_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  (s : CategoryTheory.Limits.Cone F.leftOp),
  (CategoryTheory.Limits.isLimitConeLeftOpOfCocone F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeOfConeLeftOp s)).unop
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Real.Gamma_eq_integral : ∀ {s : ℝ}, 0 < s → Real.Gamma s = ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-x) * x ^ (s - 1)
-- Mathlib.Algebra.Polynomial.Eval.Degree
/-- If `R` and `S` are isomorphic, then so are their polynomial rings.  -/
Polynomial.mapEquiv : {R : Type u} → {S : Type v} → [inst : Semiring R] → [inst_1 : Semiring S] → R ≃+* S → Polynomial R ≃+* Polynomial S
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix_symm : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁),
  (LinearMap.BilinForm.toMatrix b).symm = Matrix.toBilin b
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.norm_integral_le_of_norm_le_const : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : α → G} {C : ℝ},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → ‖∫ (x : α), f x ∂μ‖ ≤ C * μ.real Set.univ
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- `finsum`s of circle integrable functions are circle integrable.  -/
CircleIntegrable.finsum : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {c : ℂ} {R : ℝ} {ι : Type u_3} {f : ι → ℂ → E},
  (∀ (i : ι), CircleIntegrable (f i) c R) → CircleIntegrable (∑ᶠ (i : ι), f i) c R
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.continuousGeneratedBy_iff : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] (g : Y → Z),
  Topology.ContinuousGeneratedBy X g ↔
    Continuous (⇑Topology.WithGeneratedByTopology.equiv.symm ∘ g ∘ ⇑Topology.WithGeneratedByTopology.equiv)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_one_lt_lift : ∀ {o : Ordinal.{u}}, Ordinal.omega 1 < Ordinal.lift.{v, u} o ↔ Ordinal.omega 1 < o
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimits_of_hasLimits_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.Limits.HasLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ],
  CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v₁, u₁} C
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (next : Option α), sizeOf { next := next } = 1 + sizeOf next
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.JPDecl.name : Lean.Elab.Term.Do.JPDecl → Lean.Name
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.of.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K),
  GenContFract.of v =
    match GenContFract.IntFractPair.seq1 v with
    | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of `inv_neg''`. -/
inv_lt_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulMono G₀], a⁻¹ < 0 ↔ a < 0
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.NormalExpr.zero.injEq : ∀ (e e_1 : Lean.Expr), (Mathlib.Tactic.Abel.NormalExpr.zero e = Mathlib.Tactic.Abel.NormalExpr.zero e_1) = (e = e_1)
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.instBEqPolyCnstr.beq.match_1.splitter : (motive : Nat.Internal.Linear.PolyCnstr → Nat.Internal.Linear.PolyCnstr → Sort u_1) →
  (x x_1 : Nat.Internal.Linear.PolyCnstr) →
    ((a : Bool) →
        (a_1 a_2 : Nat.Internal.Linear.Poly) →
          (b : Bool) →
            (b_1 b_2 : Nat.Internal.Linear.Poly) →
              motive { eq := a, lhs := a_1, rhs := a_2 } { eq := b, lhs := b_1, rhs := b_2 }) →
      ((x x_2 : Nat.Internal.Linear.PolyCnstr) →
          (∀ (a : Bool) (a_1 a_2 : Nat.Internal.Linear.Poly) (b : Bool) (b_1 b_2 : Nat.Internal.Linear.Poly),
              x = { eq := a, lhs := a_1, rhs := a_2 } → x_2 = { eq := b, lhs := b_1, rhs := b_2 } → False) →
            motive x x_2) →
        motive x x_1
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.mk.inj : ∀ {α : Type u} {isUniformSpace : UniformSpace α} {isCompleteSpace : CompleteSpace α} {isT0 : T0Space α} {α_1 : Type u}
  {isUniformSpace_1 : UniformSpace α_1} {isCompleteSpace_1 : CompleteSpace α_1} {isT0_1 : T0Space α_1},
  { α := α, isUniformSpace := isUniformSpace, isCompleteSpace := isCompleteSpace, isT0 := isT0 } =
      { α := α_1, isUniformSpace := isUniformSpace_1, isCompleteSpace := isCompleteSpace_1, isT0 := isT0_1 } →
    α = α_1 ∧ isUniformSpace ≍ isUniformSpace_1
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.decidableEq.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : IsCancelMul α] {s : Submonoid α} [inst_2 : DecidableEq α]
  (a b : Localization s),
  a.decidableEq b = a.recOnSubsingleton₂ b fun x x_1 x_2 x_3 => decidable_of_iff' (↑x_3 * x = ↑x_2 * x_1) ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.nodup_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.keys.Nodup
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_lt_tsub_right_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], c ≤ a → a < b → a - c < b - c
-- Init.Data.List.Nat.Range
List.mem_range'_1 : ∀ {s n m : ℕ}, m ∈ List.range' s n ↔ s ≤ m ∧ m < s + n
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.IsCompressed.eq : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v : α} [inst_3 : DecidableEq α], UV.IsCompressed u v s → UV.compression u v s = s
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.elabTransparency : Lean.TSyntax `Aesop.Frontend.Parser.transparency → Lean.Elab.TermElabM Lean.Meta.TransparencyMode
-- Qq.SortLocalDecls
Qq.SortLocalDecls.Context.mk.injEq : ∀ (localDecls localDecls_1 : Lean.NameMap Lean.LocalDecl),
  ({ localDecls := localDecls } = { localDecls := localDecls_1 }) = (localDecls = localDecls_1)
-- Lean.Server.References
/-- Yields all imports that import the given `requestedMod`.  -/
Lean.Server.References.importedBy : Lean.Server.References → Lean.Name → Array Lean.Server.ModuleImport
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.re_zero : Complex.UnitDisc.re 0 = 0
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_three_mul : ∀ (x : ℝ), Real.sin (3 * x) = 3 * Real.sin x - 4 * Real.sin x ^ 3
-- Mathlib.Data.Fin.SuccPred
/-- The 'identity' equivalence between `Fin m` and `Fin n` when `m = n`.  -/
finCongr : {n m : ℕ} → n = m → Fin n ≃ Fin m
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSMul' : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_2} →
      [inst_1 : Semiring R] →
        [inst_2 : TopologicalSpace R] →
          {M : Type u_3} →
            [inst_3 : TopologicalSpace M] →
              [inst_4 : AddCommMonoid M] → [inst_5 : Module R M] → [ContinuousSMul R M] → SMul C(α, R) C(α, M)
-- Mathlib.RingTheory.Localization.Basic
/-- If `R` is a field, then localizing at a submonoid not containing `0` adds no new elements.  -/
IsField.localization_map_bijective : ∀ {R : Type u_4} {Rₘ : Type u_5} [inst : CommRing R] [inst_1 : CommRing Rₘ] {M : Submonoid R},
  0 ∉ M → IsField R → ∀ [inst_2 : Algebra R Rₘ] [IsLocalization M Rₘ], Function.Bijective ⇑(algebraMap R Rₘ)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNat.injEq : ∀ (h : Lean.Expr) (x : Int.Internal.Linear.Var) (e' : Int.Internal.Linear.Expr) (h_1 : Lean.Expr)
  (x_1 : Int.Internal.Linear.Var) (e'_1 : Int.Internal.Linear.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNat h x e' =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNat h_1 x_1 e'_1) =
    (h = h_1 ∧ x = x_1 ∧ e' = e'_1)
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.map_obj_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)} (α : F₁ ⟶ F₂)
  (t : F₁.Elements), ((CategoryTheory.CategoryOfElements.map α).obj t).fst = t.fst
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getAltDArrow : Lean.Syntax → Lean.Syntax
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.apply_mulSingle₂ : ∀ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} {O : ι → Type u_8} [inst : (i : ι) → One (M i)]
  [inst_1 : (i : ι) → One (N i)] [inst_2 : (i : ι) → One (O i)] [inst_3 : DecidableEq ι]
  (f' : (i : ι) → M i → N i → O i),
  (∀ (i : ι), f' i 1 1 = 1) →
    ∀ (i : ι) (x : M i) (y : N i) (j : ι), f' j (Pi.mulSingle i x j) (Pi.mulSingle i y j) = Pi.mulSingle i (f' i x y) j
-- Mathlib.Analysis.Calculus.Darboux
/-- **Darboux's theorem**: the image of a `Set.OrdConnected` set under `f'` is a `Set.OrdConnected`
set, `derivWithin` version.  -/
Set.OrdConnected.image_derivWithin : ∀ {f : ℝ → ℝ} {s : Set ℝ}, s.OrdConnected → DifferentiableOn ℝ f s → (derivWithin f s '' s).OrdConnected
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- The proximity function is non-negative.
 -/
ValueDistribution.proximity_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {a : WithTop E}, 0 ≤ ValueDistribution.proximity f a
-- Init.Core
instDecidableTrue : Decidable True
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.bind_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T)
  (F : (i : E.I₀) → CategoryTheory.PreZeroHypercover (E.X i)), (E.bind F).I₀ = ((i : E.I₀) × (F i).I₀)
-- Mathlib.Algebra.DirectSum.Decomposition
/-- `DirectSum.Decomposition` instances, while carrying data, are always equal.  -/
DirectSum.instSubsingletonDecomposition : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ), Subsingleton (DirectSum.Decomposition ℳ)
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.mk : ∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {f : Polynomial K},
  (Polynomial.map (algebraMap K L) f).Splits → Algebra.adjoin K (f.rootSet L) = ⊤ → Polynomial.IsSplittingField K L f
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.equivSentence.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'},
  FirstOrder.Language.Formula.equivSentence =
    (FirstOrder.Language.BoundedFormula.constantsVarsEquiv.trans
        (FirstOrder.Language.BoundedFormula.relabelEquiv (Equiv.sumEmpty α Empty))).symm
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_zero : Real.arcsin 0 = 0
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.PenroseVar.mk : String → List ℕ → Lean.Expr → Mathlib.Tactic.Widget.StringDiagram.PenroseVar
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.mk.sizeOf_spec : ∀ (lhs rhs : Lean.Expr) (rlhs rrhs : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (d : Lean.Meta.Grind.Arith.CommRing.PolyDerivation)
  (ofSemiring? : Option (Lean.Meta.Grind.Arith.CommRing.SemiringExpr × Lean.Meta.Grind.Arith.CommRing.SemiringExpr)),
  sizeOf { lhs := lhs, rhs := rhs, rlhs := rlhs, rrhs := rrhs, d := d, ofSemiring? := ofSemiring? } =
    1 + sizeOf lhs + sizeOf rhs + sizeOf rlhs + sizeOf rrhs + sizeOf d + sizeOf ofSemiring?
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- A function is almost everywhere measurable if it coincides almost everywhere with a measurable
function.

A similar notion is `MeasureTheory.NullMeasurable`. That notion is equivalent to `AEMeasurable` if
the σ-algebra on the codomain is countably generated, but weaker in general.  -/
AEMeasurable : {α : Type u_1} →
  {β : Type u_2} →
    [MeasurableSpace β] →
      {_m : MeasurableSpace α} → (α → β) → autoParam (MeasureTheory.Measure α) AEMeasurable._auto_1 → Prop
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_zero : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → Zero (G i)] [inst_7 : Zero C] [∀ (i : ι), ZeroHomClass (H i) (G i) C]
  [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] (g : (i : ι) → H i)
  (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)), DirectLimit.lift f (fun x => ⇑(g x)) h 0 = 0
-- Mathlib.RingTheory.Grassmannian
/-- `G(k, M; R)` is the `k`ᵗʰ Grassmannian of the `R`-module `M`. It is defined to be the set of
submodules of `M` whose quotient is locally free of rank `k`. Note that there is another convention
in literature where instead the submodule is required to have rank `k`. See the module docstring
of `RingTheory.Grassmannian`.  -/
Module.Grassmannian : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [Module R M] → ℕ → Type v
-- Mathlib.Topology.Connected.PathConnected
pathComponentIn_nonempty_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {F : Set X}, (pathComponentIn F x).Nonempty ↔ x ∈ F
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Mono.of_coproductDisjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C}
  [CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X}
  (hc : CategoryTheory.Limits.IsColimit c) (i : ι), CategoryTheory.Mono (c.inj i)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.ker_coprod_of_disjoint_range : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁] [inst_9 : AddCommGroup M₂]
  [inst_10 : Module R M₂] {f₁ : M₁ →L[R] M} {f₂ : M₂ →L[R] M},
  Disjoint (↑f₁).range (↑f₂).range → (↑(f₁.coprod f₂)).ker = (↑f₁).ker.prod (↑f₂).ker