mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_zsmul_sub_toIcoMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp a b • p + toIcoMod hp a b = b
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.filter₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {f : (a : α) → β a → Bool}, m.WF → (↑(Std.DHashMap.Internal.Raw₀.filter f ⟨m, h⟩)).WF
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblX.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P : Fin 3 → R),
  W'.dblX P =
    W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P 2 * (P 1 - W'.negY P) - W'.a₂ * P 2 ^ 2 * (P 1 - W'.negY P) ^ 2 -
      2 * P 0 * (P 1 - W'.negY P) ^ 2
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_real_closedBall' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) {r : ℝ},
  0 ≤ r → μ.real (Metric.closedBall x r) = r ^ Module.finrank ℝ E * μ.real (Metric.closedBall 0 1)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (U : CategoryTheory.Comonad C) → C → CategoryTheory.Cokleisli U
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_empty : ∀ {α : Type u_1}, ∅ᶜ = Set.univ
-- Lean.Meta.CoeAttr
Lean.Meta.instReprCoeFnInfo : Repr Lean.Meta.CoeFnInfo
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_eq_empty : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support = ∅ ↔ p = 0
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.ediam_image_inter_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X}, HolderOnWith C r f s → ∀ (t : Set X), Metric.ediam (f '' (t ∩ s)) ≤ ↑C * Metric.ediam t ^ ↑r
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.coe_lineal : ∀ {R : Type u_1} {E : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] (C : PointedCone R E), ↑C.lineal = ↑C ∩ -↑C
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Applying `lower F` and then `representative` is isomorphic to first applying `representative`
and then applying `F`.
 -/
CategoryTheory.Subobject.lowerCompRepresentativeIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (F : CategoryTheory.Functor (CategoryTheory.MonoOver Y) (CategoryTheory.MonoOver X)) →
        (CategoryTheory.Subobject.lower F).comp CategoryTheory.Subobject.representative ≅
          CategoryTheory.Subobject.representative.comp F
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insertC.go : Lean.Grind.CommRing.Mon → ℕ → ℤ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Logic.Embedding.Basic
Equiv.coeEmbedding : {α : Sort u} → {β : Sort v} → Coe (α ≃ β) (α ↪ β)
-- Mathlib.Data.List.Destutter
List.destutter'_nil : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a : α}, List.destutter' R a [] = [a]
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.brecOn.eq : ∀ {motive_1 : Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Sort u}
  {motive_3 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  {motive_4 : Task Lean.Language.Lean.CommandParsedSnapshot → Sort u} (t : Lean.Language.Lean.CommandParsedSnapshot)
  (F_1 : (t : Lean.Language.Lean.CommandParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
      Lean.Language.Lean.CommandParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
      Lean.Language.Lean.CommandParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Task Lean.Language.Lean.CommandParsedSnapshot) →
      Lean.Language.Lean.CommandParsedSnapshot.below_3 t → motive_4 t),
  t.brecOn F_1 F_2 F_3 F_4 = F_1 t (Lean.Language.Lean.CommandParsedSnapshot.brecOn.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.tensorHom_def : ∀ (R : Type u) [inst : CommRing R] {X₁ Y₁ X₂ Y₂ : CoalgCat R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    CoalgCat.ofHom (Coalgebra.TensorProduct.map f.toCoalgHom' g.toCoalgHom')
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.eq : ∀ (S : Set ℕ) {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
  (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension S A ↥C₁] [h₂ : IsCyclotomicExtension S A ↥C₂], C₁ = C₂
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.section_.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [hf : CategoryTheory.IsSplitEpi f], CategoryTheory.section_ f = CategoryTheory.section_ f_1
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LEquiv.onTerm_apply : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (φ : L ≃ᴸ L') (a : L.Term α),
  φ.onTerm a = φ.toLHom.onTerm a
-- Mathlib.Algebra.Group.Action.Defs
vadd_neg_vadd : ∀ {G : Type u_3} {α : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (a : α), g +ᵥ -g +ᵥ a = a
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearMap.iSupIndep_map : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Function.Injective ⇑f → ∀ {m : ι → Submodule R M}, iSupIndep m → iSupIndep fun i => Submodule.map f (m i)
-- Mathlib.Order.CompleteLattice.Basic
sInf_apply : ∀ {α : Type u_8} {β : α → Type u_9} [inst : (i : α) → InfSet (β i)] {s : Set ((a : α) → β a)} {a : α},
  sInf s a = ⨅ f, ↑f a
-- Mathlib.Data.List.Cycle
Cycle.chain_map : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (f : β → α) {s : Cycle β},
  Cycle.Chain r (Cycle.map f s) ↔ Cycle.Chain (fun a b => r (f a) (f b)) s
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.norm_eq_one_iff : ∀ (z : ℂ), ‖z‖ = 1 ↔ ∃ θ, Complex.exp (↑θ * Complex.I) = z
-- Mathlib.Algebra.Module.End
/-- A convenience alias for `Module.toAddMonoidEnd` as an `AddMonoidHom`, usually to allow the
use of `AddMonoidHom.flip`.  -/
smulAddHom : (R : Type u_1) → (M : Type u_3) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → R →+ M →+ M
-- Mathlib.Order.Interval.Set.Basic
Set.mem_Ici_of_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a x : α}, x ∈ Set.Ioi a → x ∈ Set.Ici a
-- Init.Data.Nat.Gcd
Nat.gcd_mul_left_sub_left : ∀ {m n k : ℕ}, n ≤ m * k → (m * k - n).gcd m = n.gcd m
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerTMul_add : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β] (A : Matrix l m α) (B₁ B₂ : Matrix n p β),
  Matrix.kroneckerMap (TensorProduct.tmul R) A (B₁ + B₂) =
    Matrix.kroneckerMap (TensorProduct.tmul R) A B₁ + Matrix.kroneckerMap (TensorProduct.tmul R) A B₂
-- Mathlib.Data.Fintype.Sum
/-- If the subtype of all-but-one elements is a `Fintype` then the type itself is a `Fintype`.  -/
fintypeOfFintypeNe : {α : Type u_1} → (a : α) → Fintype { b // b ≠ a } → Fintype α
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.add` -/
Meromorphic.fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E}, Meromorphic f → Meromorphic g → Meromorphic fun i => f i + g i
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- An affine map from a finite-dimensional space is automatically Lipschitz.  -/
AffineMap.lipschitzWith_of_finiteDimensional : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  {PE : Type u_1} {PF : Type u_2} [inst_6 : MetricSpace PE] [inst_7 : NormedAddTorsor E PE] [inst_8 : MetricSpace PF]
  [inst_9 : NormedAddTorsor F PF] [FiniteDimensional 𝕜 E] (f : PE →ᵃ[𝕜] PF), ∃ K, LipschitzWith K ⇑f
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.instContinuousLinearEquivClass : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W}, ContinuousLinearEquivClass (σ.Equiv ρ) R W V
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivAt.prodMap : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] {f : E → F} {f' : E →L[𝕜] F} {f₂ : G → G'} {f₂' : G →L[𝕜] G'} (p : E × G),
  HasFDerivAt f f' p.1 → HasFDerivAt f₂ f₂' p.2 → HasFDerivAt (Prod.map f f₂) (f'.prodMap f₂') p
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mu_toDual : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq α] (a b : α),
  (IncidenceAlgebra.mu 𝕜) (OrderDual.toDual a) (OrderDual.toDual b) = (IncidenceAlgebra.mu 𝕜) b a
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom.sizeOf_spec : ∀ (α : Mathlib.Tactic.BicategoryLike.StructuralAtom),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom α) = 1 + sizeOf α
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.completeSpace : ∀ (X : CpltSepUniformSpace), CompleteSpace X.toUniformSpace.carrier
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.startsWith_slice_eq_false_iff : ∀ {pat s : String.Slice}, s.startsWith pat = false ↔ ¬pat.copy.toList <+: s.copy.toList
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The monoidal category instance.  -/
Mathlib.Tactic.Monoidal.Context.instMonoidal? : (self : Mathlib.Tactic.Monoidal.Context) → Option Q(CategoryTheory.MonoidalCategory unknown_1)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Alt.vars : {σ : Type} → Lean.Elab.Term.Do.Alt σ → Array Lean.Elab.Term.Do.Var
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `>>=`, general version.  -/
SatisfiesM.bind : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} {p : α → Prop} {x : m α} {q : β → Prop} [inst : Monad m] [LawfulMonad m]
  {f : α → m β}, SatisfiesM p x → (∀ (a : α), p a → SatisfiesM q (f a)) → SatisfiesM q (x >>= f)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Any costructured arrow factors through a universal arrow.  -/
CategoryTheory.CostructuredArrow.IsUniversal.fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal)
  (g : CategoryTheory.CostructuredArrow S T), CategoryTheory.CategoryStruct.comp (S.map (h.lift g)) f.hom = g.hom
-- Mathlib.AlgebraicGeometry.ResidueField
/-- If `X ⟶ Y` is a morphism of locally ringed spaces and `x` a point of `X`, we obtain
a morphism of residue fields in the other direction.  -/
AlgebraicGeometry.Scheme.Hom.residueFieldMap : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → (x : ↥X) → Y.residueField (f x) ⟶ X.residueField x
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.finrank_range_dualMap_eq_finrank_range : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] (f : V₁ →ₗ[K] V₂),
  Module.finrank K ↥f.dualMap.range = Module.finrank K ↥f.range
-- Std.Data.ExtTreeSet.Lemmas
_private.Std.Data.ExtTreeSet.Lemmas.0.Std.ExtTreeSet.ext_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t t' : Std.ExtTreeSet α cmp}, t = t' ↔ t.inner = t'.inner
-- Mathlib.SetTheory.Ordinal.Basic
/-- Note that the presence of this lemma makes `simp [omega0]` form a loop.  -/
Ordinal.type_nat_lt : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.omega0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInsertReplaceEdit.toJson : Lean.Lsp.InsertReplaceEdit → Lean.Json
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_mem_set : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} [WellFoundedLT ι], (∃ j, n ≤ j ∧ u j ω ∈ s) → u (MeasureTheory.hittingAfter u s n ω).untopA ω ∈ s
-- Mathlib.CategoryTheory.Subfunctor.Finite
/-- A subpresheaf `G : Subfunctor F` is generated by sections `x i : F.obj (X i)`
if `⨆ (i : ι), ofSection (x i) = G`.  -/
CategoryTheory.Subfunctor.IsGeneratedBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      CategoryTheory.Subfunctor F → {ι : Type w'} → {X : ι → Cᵒᵖ} → ((i : ι) → F.obj (X i)) → Prop
-- Mathlib.CategoryTheory.Abelian.CommSq
/-- Given a pushout square in an abelian category
```
X₁ ⟶ X₂
|    |
v    v
X₃ ⟶ X₄
```
the morphism `X₂ ⊞ X₃ ⟶ X₄` is an epimorphism. This lemma translates this
as the existence of liftings up to refinements: a morphism `z : T ⟶ X₄`
can be written as a sum of a morphism to `X₂` and a morphism to `X₃`,
at least if we allow a precomposition with an epimorphism `π : T' ⟶ T`.  -/
CategoryTheory.IsPushout.hom_eq_add_up_to_refinements : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X₁ X₂ X₃ X₄ : C}
  {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPushout t l r b →
    ∀ {T : C} (x₄ : T ⟶ X₄),
      ∃ T' π,
        ∃ (_ : CategoryTheory.Epi π),
          ∃ x₂ x₃,
            CategoryTheory.CategoryStruct.comp π x₄ =
              CategoryTheory.CategoryStruct.comp x₂ r + CategoryTheory.CategoryStruct.comp x₃ b
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.trivial_eq_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.GrothendieckTopology.trivial C = ⊥
-- Mathlib.Analysis.Complex.Norm
Complex.norm_sub_one_sq_eq_of_norm_eq_one : ∀ {z : ℂ}, ‖z‖ = 1 → ‖z - 1‖ ^ 2 = 2 * (1 - z.re)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.length_transfer : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet),
  (p.transfer H hp).length = p.length
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_eq_one_iff_existsUnique_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V} [inst : Fintype ↑(G.neighborSet v)], G.degree v = 1 ↔ ∃! w, G.Adj v w
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If 0 belongs to the interior of `integrableExpSet X μ`, then `X` is in `ℒp` for all
finite `p`.  -/
ProbabilityTheory.memLp_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  0 ∈ interior (ProbabilityTheory.integrableExpSet X μ) → ∀ (p : NNReal), MeasureTheory.MemLp X (↑p) μ
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) {κ : Type u_5} {f : κ → ι}
  (hf : Function.Injective f) (hcompl : IsCompl (Set.range f) (Set.range P.map)) (k : κ),
  (P.basisKaehlerOfIsCompl hf hcompl) k = (KaehlerDifferential.D R S) (P.val (f k))
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.CommRingCat.Hom.mk : {R S : CommRingCat} → (↑R →+* ↑S) → R.Hom S
-- Init.Data.Vector.Attach
Vector.getElem_attachWith : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {P : α → Prop} {H : ∀ a ∈ xs, P a} {i : ℕ} (h : i < n),
  (xs.attachWith P H)[i] = ⟨xs[i], ⋯⟩
-- Mathlib.Topology.Constructions
Finset.continuous_restrict_apply : ∀ {X : Type u} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] (s : Finset X) {f : X → Z},
  Continuous f → Continuous (s.restrict f)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.getTerm.go : ℕ → Lean.Meta.Grind.SolverTerms → Option Lean.Expr
-- Mathlib.RingTheory.PolynomialAlgebra
instIsPushoutPolynomial_1 : ∀ (R : Type u_1) [inst : CommSemiring R] {S : Type u_4} [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.IsPushout R (Polynomial R) S (Polynomial S)
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.mem_space_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {x : E}, x ∈ K.space ↔ ∃ s ∈ K.faces, x ∈ (convexHull 𝕜) ↑s
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResult.subgoal : Lean.MVarId → Array Lean.FVarId → List Lean.Name → Lean.Meta.InjectionResult
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.sum_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddCommMonoid β]
  [inst_3 : ContinuousAdd β] {ι : Type u_3} (s : Finset ι) (f : ι → C(α, β)) (a : α),
  (∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a
-- Mathlib.Order.Bounds.Basic
/-- Sets are automatically bounded or cobounded in complete lattices. To use the same statements
in complete and conditionally complete lattices but let automation fill automatically the
boundedness proofs in complete lattices, we use the tactic `bddDefault` in the statements,
in the form `(hA : BddAbove A := by bddDefault)`.  -/
tacticBddDefault : Lean.ParserDescr
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?_cons : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α}
  {xs : List α},
  List.maxIdxOn? f (x :: xs) =
    some (if h : xs = [] then 0 else if f (List.maxOn f xs h) ≤ f x then 0 else List.maxIdxOn f xs h + 1)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_sup_distrib_left : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α),
  a ⊔ s.inf' hs f = s.inf' hs fun i => a ⊔ f i
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.truncTotal_subst_eq_truncTotal_subst_sum : ∀ {σ : 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)
          (MvPowerSeries.subst a (∑ i ∈ Finset.range k, (MvPowerSeries.homogeneousComponent i) f))
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.log_rpow : ∀ {x : ℝ}, 0 < x → ∀ (y : ℝ), Real.log (x ^ y) = y * Real.log x
-- Mathlib.Algebra.Category.AlgCat.Limits
/-- Witness that the limit cone in `AlgCat R` is a limit cone.
(Internal use only; use the limits API.)
 -/
AlgCat.HasLimits.limitConeIsLimit : {R : Type u} →
  [inst : CommRing R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (AlgCat R)) →
          [inst_2 : Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] →
            CategoryTheory.Limits.IsLimit (AlgCat.HasLimits.limitCone F)
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
IsIntegral.of_pow : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B} {n : ℕ},
  0 < n → IsIntegral R (x ^ n) → IsIntegral R x
-- Mathlib.Algebra.Group.Units.Defs
/-- `neg` is the right additive inverse of `val` in the base `AddMonoid`.  -/
AddUnits.val_neg : ∀ {α : Type u} [inst : AddMonoid α] (self : AddUnits α), ↑self + self.neg = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.instDecidableEqKey : DecidableEq Std.Tactic.BVDecide.BVExpr.Cache.Key
-- Batteries.Tactic.GeneralizeProofs
/-- Core implementation of abstracting a proof.
 -/
_private.Batteries.Tactic.GeneralizeProofs.0.Batteries.Tactic.GeneralizeProofs.abstractProofs.visitProof : Lean.Expr → Option Lean.Expr → Batteries.Tactic.GeneralizeProofs.MAbs Lean.Expr
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The isomorphism between the `n`-th Tate cohomology and `n`-th group cohomology for `n : ℕ`
non-zero.  -/
TateCohomology.isoGroupCohomology : {R G : Type u} →
  [inst : CommRing R] →
    [inst_1 : Group G] →
      [inst_2 : Fintype G] → (n : ℕ) → [NeZero n] → tateCohomologyFunctor ↑n ≅ groupCohomology.functor R G n
-- Init.Data.Vector.Find
Vector.find?_flatMap_eq_none_iff : ∀ {α : Type u_1} {n : ℕ} {β : Type} {m : ℕ} {xs : Vector α n} {f : α → Vector β m} {p : β → Bool},
  Vector.find? p (xs.flatMap f) = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, (!p y) = true
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- A word and its maximal reduction correspond to the same element of the additive
free group.  -/
FreeAddGroup.reduce.self : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.mk (FreeAddGroup.reduce L) = FreeAddGroup.mk L
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.Hom.ext : ∀ {A B : CommGrpCat} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.addMonoidWithOne : {R : Type u} → {M : Type v} → [AddMonoidWithOne R] → [AddMonoid M] → AddMonoidWithOne (TrivSqZeroExt R M)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {r : Std.Rci α} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxi.HasSize α]
  [Std.Rxi.LawfulHasSize α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxi.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α], r.isEmpty = true ↔ ∀ (a : α), a ∉ r
-- Init.Data.Float.Model.Format.Basic
/-- The number of bits in the mantissa, *excluding the implicit bit*.  -/
Float.Model.Format.mantissaBitsWithoutImplicit : Float.Model.Format → ℕ
-- Mathlib.Algebra.Module.Presentation.Differentials
Algebra.Presentation.differentials.hom₁.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ),
  Algebra.Presentation.differentials.hom₁ pres =
    Finsupp.linearCombination S fun r => Algebra.Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Functor.toCostructuredArrow_comp_proj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C)
  (F : CategoryTheory.Functor C D) (X : D) (f : (Y : E) → F.obj (G.obj Y) ⟶ X)
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y),
  (G.toCostructuredArrow F X f ⋯).comp (CategoryTheory.CostructuredArrow.proj F X) = G
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instPartialOrder.eq_1 : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G],
  ClosedSubgroup.instPartialOrder G = PartialOrder.ofSetLike (ClosedSubgroup G) G