mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Abs
ContDiffWithinAt.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ∞} {f : E → ℝ} {s : Set E} {x : E},
  ContDiffWithinAt ℝ (↑n) f s x → f x ≠ 0 → ContDiffWithinAt ℝ (↑n) (fun y => |f y|) s x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_const : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] (b : M), ∑ _x ∈ s, b = s.card • b
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonWaitForILeansParams : Lean.ToJson Lean.Lsp.WaitForILeansParams
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist_self : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V}, G.dist v v = 0
-- Lean.Expr
Lean.BinderInfo.strictImplicit.sizeOf_spec : sizeOf Lean.BinderInfo.strictImplicit = 1
-- Mathlib.Topology.Algebra.StarSubalgebra
/-- Continuous `StarAlgHom`s from the topological closure of a `StarSubalgebra` whose
compositions with the `StarSubalgebra.inclusion` map agree are, in fact, equal.  -/
StarAlgHom.ext_topologicalClosure : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A]
  [inst_6 : StarModule R A] [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A]
  [inst_9 : TopologicalSpace B] [inst_10 : Semiring B] [inst_11 : Algebra R B] [inst_12 : StarRing B] [T2Space B]
  {S : StarSubalgebra R A} {φ ψ : ↥S.topologicalClosure →⋆ₐ[R] B},
  Continuous ⇑φ → Continuous ⇑ψ → φ.comp (StarSubalgebra.inclusion ⋯) = ψ.comp (StarSubalgebra.inclusion ⋯) → φ = ψ
-- Init.Data.Int.Lemmas
Int.negOfNat_eq_subNatNat_zero : ∀ (n : ℕ), Int.negOfNat n = Int.subNatNat 0 n
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrict'.eq_1 : ∀ (A : Type u_1) {K : Type u_2} {L : Type u_3} {L₂ : Type u_4} (B : Type u_6) (B₂ : Type u_7) [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : Algebra K L] [inst_10 : Algebra A L]
  [inst_11 : IsScalarTower A K L] [inst_12 : Algebra K L₂] [inst_13 : Algebra A L₂] [inst_14 : IsScalarTower A K L₂]
  [inst_15 : Algebra B L] [inst_16 : IsScalarTower A B L] [inst_17 : IsIntegralClosure B A L] [inst_18 : Algebra B₂ L₂]
  [inst_19 : IsScalarTower A B₂ L₂] [inst_20 : IsIntegralClosure B₂ A L₂] (f : L →ₐ[K] L₂),
  galRestrict' A B B₂ f =
    (↑(IsIntegralClosure.equiv A (↥(integralClosure A L₂)) L₂ B₂)).comp
      (((AlgHom.restrictScalars A f).comp (IsScalarTower.toAlgHom A B L)).codRestrict (integralClosure A L₂) ⋯)
-- Mathlib.Algebra.Group.End
Equiv.Perm.inv_trans_self : ∀ {α : Type u_4} (e : Equiv.Perm α), Equiv.trans e⁻¹ e = 1
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
ConditionallyCompleteLinearOrder.toLinearOrder : {α : Type u_1} → [h : ConditionallyCompleteLinearOrder α] → LinearOrder α
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.symm_trans_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {L : Type u_3} [inst_4 : Add L] [inst_5 : TopologicalSpace L] (e₁ : M ≃ₜ+ N) (e₂ : N ≃ₜ+ L) (l : L),
  (e₁.trans e₂).symm l = e₁.symm (e₂.symm l)
-- Mathlib.Analysis.Convex.Between
AffineEquiv.wbtw_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {x y z : P} (f : P ≃ᵃ[R] P'),
  Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z
-- Mathlib.Topology.Order.LiminfLimsup
Pi.instBoundedLENhdsClass : ∀ {ι : Type u_1} {π : ι → Type u_6} [Finite ι] [inst : (i : ι) → Preorder (π i)]
  [inst_1 : (i : ι) → TopologicalSpace (π i)] [∀ (i : ι), BoundedLENhdsClass (π i)], BoundedLENhdsClass ((i : ι) → π i)
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.constSDiv_symm_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalTorsor P] (p : P) (x : V),
  (Homeomorph.constSDiv p).symm x = x⁻¹ • p
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.TZSpec.filePath.injEq : ∀ (p p_1 : String), (Std.Time.Database.TZdb.TZSpec.filePath p = Std.Time.Database.TZdb.TZSpec.filePath p_1) = (p = p_1)
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
/-- If `M` is a submodule in an algebra `S` over `R`,
there is the natural isomorphism of `R`-modules between
`M ⊗[R] i(R)` and `M` induced by multiplication in `S`, here `i : R → S` is the structure map.
This generalizes `TensorProduct.rid` as `i(R)` is not necessarily isomorphic to `R`.  -/
Submodule.rTensorOne : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (M : Submodule R S) → TensorProduct R ↥M ↥⊥ ≃ₗ[R] ↥M
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.mk.inj : ∀ {R : Type u_2} {inst : NonAssocRing R} {toMulRingSeminorm : MulRingSeminorm R}
  {eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0} {toMulRingSeminorm_1 : MulRingSeminorm R}
  {eq_zero_of_map_eq_zero'_1 : ∀ (x : R), toMulRingSeminorm_1.toFun x = 0 → x = 0},
  { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
      { toMulRingSeminorm := toMulRingSeminorm_1, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 } →
    toMulRingSeminorm = toMulRingSeminorm_1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.coe_srange : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), ↑f.srange = Set.range ⇑f
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_three : ∀ {M : Type u_2} [inst : CommMonoid M] (f : Fin 3 → M), ∏ i, f i = f 0 * f 1 * f 2
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatch_iff : ∀ {pat s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos ↔ (s.sliceTo pos).copy = pat.copy
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- The groups `GL n R` (notation for `Matrix.GeneralLinearGroup n R`) and
`LinearMap.GeneralLinearGroup R (n → R)` are multiplicatively equivalent  -/
Matrix.GeneralLinearGroup.toLin : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → GL n R ≃* LinearMap.GeneralLinearGroup R (n → R)
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
Nat.Partition.hasProd_genFun : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R),
  HasProd (fun i => 1 + ∑' (j : ℕ), f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1))) (Nat.Partition.genFun f)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.maxValueSealed_def : Int32.maxValueSealed✝ = Int32.maxValue
-- Std.Async.Signal
/-- Bad system call.
 -/
Std.Async.Signal.sigsys : Std.Async.Signal
-- Mathlib.Data.Set.Prod
Set.eval_image_univ_pi_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {i : ι}, Function.eval i '' Set.univ.pi t ⊆ t i
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp},
  t₁.WF → (t₁ \ t₂).WF
-- Lean.Meta.Canonicalizer
_private.Lean.Meta.Canonicalizer.0.Lean.Meta.Canonicalizer.canon.unsafe_impl_2 : UInt64 → Lean.Meta.Canonicalizer.State → Option (List Lean.Expr)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isSome_minKey?_modifyKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β}
  {l : List ((_ : α) × β)}, (Std.Internal.List.minKey? (Std.Internal.List.Const.modifyKey k f l)).isSome = !l.isEmpty
-- Init.Data.Slice.Array.Lemmas
Array.toList_mkSlice_rii : ∀ {α : Type u_1} {xs : Array α}, Std.Slice.toList (Std.Rii.Sliceable.mkSlice xs *...*) = xs.toList
-- Mathlib.Analysis.Seminorm
/-- The composition as an `AddMonoidHom`.  -/
Seminorm.pullback : {𝕜 : Type u_3} →
  {𝕜₂ : Type u_4} →
    {E : Type u_7} →
      {E₂ : Type u_8} →
        [inst : SeminormedRing 𝕜] →
          [inst_1 : SeminormedRing 𝕜₂] →
            {σ₁₂ : 𝕜 →+* 𝕜₂} →
              [RingHomIsometric σ₁₂] →
                [inst_3 : AddCommGroup E] →
                  [inst_4 : AddCommGroup E₂] →
                    [inst_5 : Module 𝕜 E] → [inst_6 : Module 𝕜₂ E₂] → (E →ₛₗ[σ₁₂] E₂) → Seminorm 𝕜₂ E₂ →+ Seminorm 𝕜 E
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.EStateM.tryCatch.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)) (h_2 : (ok : EStateM.Result ε σ α) → motive ok),
  (match EStateM.Result.error e s with
    | EStateM.Result.error e s => h_1 e s
    | ok => h_2 ok) =
    h_1 e s
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The ring homomorphism from the preimage of `s` to `s`.  -/
RingHom.restrict : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] →
        {σR : Type u_1} →
          {σS : Type u_2} →
            [inst_2 : SetLike σR R] →
              [inst_3 : SetLike σS S] →
                [inst_4 : SubsemiringClass σR R] →
                  [inst_5 : SubsemiringClass σS S] →
                    (f : R →+* S) → (s' : σR) → (s : σS) → (∀ x ∈ s', f x ∈ s) → ↥s' →+* ↥s
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- The Dirichlet density is nonnegative.  -/
NumberField.Set.HasDirichletDensity.nonneg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ},
  NumberField.Set.HasDirichletDensity S δ → 0 ≤ δ
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` which has coproducts is said to have `AB4` of size `w` provided that
coproducts of size `w` are exact.
 -/
CategoryTheory.AB4OfSize : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasCoproducts C] → Prop
-- Batteries.Data.Fin.Lemmas
Fin.countP_succ : ∀ {n : ℕ} (p : Fin (n + 1) → Bool), Fin.countP p = (p 0).toNat + Fin.countP fun x => p x.succ
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.isRoot_map_iff : ∀ {S : Type v} [inst : CommSemiring S] {R : Type u_1} [inst_1 : CommRing R] {f : R →+* S} {x : R} {p : Polynomial R},
  Function.Injective ⇑f → ((Polynomial.map f p).IsRoot (f x) ↔ p.IsRoot x)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.experimental? : Lean.Lsp.ServerCapabilities → Option Lean.Lsp.LeanServerCapabilities
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.map_nonunit : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') {a : R},
  ¬IsUnit a → χ a = 0
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `val_v(v^n) = n` for every `n ∈ ℕ`.  -/
FractionalIdeal.count_pow_self : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℕ),
  FractionalIdeal.count K v (↑v.asIdeal ^ n) = ↑n
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- An injective equivariant map `α →ₑ[σ] β` induces
an equivariant map on embedding types `(ι ↪ α) → (ι ↪ β)`.  -/
Function.Injective.addActionHom_embedding : {G : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G α] →
        {H : Type u_3} →
          {β : Type u_4} →
            [inst_2 : AddGroup H] →
              [inst_3 : AddAction H β] →
                {σ : G → H} → {f : α →ₑ[σ] β} → (ι : Type u_5) → Function.Injective ⇑f → (ι ↪ α) →ₑ[σ] ι ↪ β
-- Init.Data.List.Lemmas
List.reverse_reverse : ∀ {α : Type u_1} (as : List α), as.reverse.reverse = as
-- Mathlib.Data.Finset.Sym
Finset.sym2_empty : ∀ {α : Type u_1}, ∅.sym2 = ∅
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertManyIfNewUnit_list_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α}, m.insertManyIfNewUnit l = ∅ ↔ m = ∅ ∧ l = []
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
TopologicalSpace.denseSeq.congr_simp : ∀ (α : Type u) [t : TopologicalSpace α] [inst : TopologicalSpace.SeparableSpace α] [inst_1 : Nonempty α] (a a_1 : ℕ),
  a = a_1 → TopologicalSpace.denseSeq α a = TopologicalSpace.denseSeq α a_1
-- Mathlib.GroupTheory.Nilpotent
/-- If the quotient by `center G` is nilpotent, then so is G.  -/
AddGroup.of_quotient_center_nilpotent : ∀ {G : Type u_1} [inst : AddGroup G], AddGroup.IsNilpotent (G ⧸ AddSubgroup.center G) → AddGroup.IsNilpotent G
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {H H_1 : J.OneHypercoverFamily} (e_H : H = H_1)
  {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C}
  {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S)
  (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)),
  CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift hP hE le F =
    CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift ⋯ ⋯ le F
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffOn_extChartAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {x : M} [IsManifold I n M],
  ContMDiffOn I (modelWithCornersSelf 𝕜 E) n (↑(extChartAt I x)) (chartAt H x).source
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomain.eq_1 : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (x : MonoidAlgebra R M),
  MonoidAlgebra.mapDomain f x = MonoidAlgebra.ofCoeff (Finsupp.mapDomain f x.coeff)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.discreteEquiv_symm_apply_as : ∀ {α : Type u₁} (as : α), (CategoryTheory.discreteEquiv.symm as).as = as
-- Std.Http.Data.Headers
/-- Updates all the values of a header if it exists.
 -/
Std.Http.Headers.update : Std.Http.Headers → Std.Http.Header.Name → (Std.Http.Header.Value → Std.Http.Header.Value) → Std.Http.Headers
-- Mathlib.Algebra.PresentedMonoid.Basic
/-- The generators of a presented additive monoid generate the
presented additive monoid. That is, the additive submonoid closure of the set of generators equals
`⊤`.  -/
PresentedAddMonoid.closure_range_of : ∀ {α : Type u_2} (rels : FreeAddMonoid α → FreeAddMonoid α → Prop),
  AddSubmonoid.closure (Set.range (PresentedAddMonoid.of rels)) = ⊤
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_sup' : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s),
  f b ≤ s.sup' ⋯ f
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toMonComon_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  (CategoryTheory.Bimon.toMonComon C).obj M = M.toMonComonObj
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_of_contains_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, (m.insert k v).contains a = true → (k == a) = false → m.contains a = true
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertMany_append : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l₁ l₂ : List (α × β)}, t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.injective_toBoundedContinuousFunctionCLM : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F],
  Function.Injective ⇑(TestFunction.toBoundedContinuousFunctionCLM 𝕜)
-- Mathlib.Tactic.Ring.Common
/-- Given monomials `va, vb`, attempts to add them together to get another monomial.
If the monomials are not compatible, returns `none`.
For example, `xy + 2xy = 3xy` is a `.nonzero` overlap, while `xy + xz` returns `none`
and `xy + -xy = 0` is a `.zero` overlap.
 -/
Mathlib.Tactic.Ring.Common.evalAddOverlap : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExProd bt sα a →
                Mathlib.Tactic.Ring.Common.ExProd bt sα b →
                  OptionT Lean.MetaM (Mathlib.Tactic.Ring.Common.Overlap bt sα q(«$a» + «$b»))
-- Init.Data.Array.Lemmas
Array.filter_push_of_pos : ∀ {α : Type u_1} {stop : ℕ} {p : α → Bool} {a : α} {xs : Array α},
  p a = true → stop = xs.size + 1 → Array.filter p (xs.push a) 0 stop = (Array.filter p xs).push a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → t.getKey? a = none
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables for monotone functions.
If `f` is continuous on `[a, b]` and has a nonnegative derivative `f'` in `(a, b)`,
then we can substitute `u = f x` to get `∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.  -/
intervalIntegral.integral_deriv_smul_comp_of_deriv_nonneg : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), 0 ≤ f' x) → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- The submodule of self-adjoint matrices with respect to the bilinear form corresponding to
the matrix `J`.  -/
selfAdjointMatricesSubmodule' : {R₂ : Type u_3} →
  [inst : CommRing R₂] → {n : Type u_5} → [Fintype n] → Matrix n n R₂ → [DecidableEq n] → Submodule R₂ (Matrix n n R₂)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.Const.beq.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : BEq β]
  (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β),
  Std.DHashMap.Internal.Raw₀.Const.beq m₁ m₂ =
    if (↑m₁).size ≠ (↑m₂).size then false else (↑m₁).all fun k v => Std.DHashMap.Internal.Raw₀.Const.get? m₂ k == some v
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- A column partitioned matrix when transposed gives a row partitioned matrix with columns of the
initial matrix transposed to become rows.  -/
Matrix.transpose_fromCols : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R),
  (A₁.fromCols A₂).transpose = A₁.transpose.fromRows A₂.transpose
-- Mathlib.Data.Multiset.ZeroCons
Multiset.instOrderBot : {α : Type u_1} → OrderBot (Multiset α)
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.lift_def : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : IsSepClosed M] [inst_6 : Algebra.IsSeparable K L],
  IsSepClosed.lift = Classical.choice ⋯
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasFDerivAt_exp_smul_const' : ∀ (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedCommRing 𝕊] [inst_2 : NormedRing 𝔸]
  [inst_3 : NormedAlgebra 𝕂 𝕊] [inst_4 : NormedAlgebra 𝕂 𝔸] [inst_5 : Algebra 𝕊 𝔸] [inst_6 : ContinuousSMul 𝕊 𝔸]
  [inst_7 : IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊),
  HasFDerivAt (fun u => NormedSpace.exp (u • x))
    ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp (t • x))) t
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁.eq_8 : ∀ (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.Λ'.ret k) = {Turing.PartrecToTM2.Λ'.ret k}
-- Mathlib.LinearAlgebra.Determinant
/-- The determinant of a family of vectors with respect to some basis, as an alternating
multilinear map.  -/
Module.Basis.det : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {ι : Type u_4} → [DecidableEq ι] → [Fintype ι] → Module.Basis ι R M → M [⋀^ι]→ₗ[R] R
-- Mathlib.Algebra.Group.Subgroup.Map
/-- The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup
generated by the image of the set.  -/
MonoidHom.map_closure : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (s : Set G),
  Subgroup.map f (Subgroup.closure s) = Subgroup.closure (⇑f '' s)
-- Lean.Data.DeclarationRange
/-- See `charUtf16`.  -/
Lean.DeclarationRange.endCharUtf16 : Lean.DeclarationRange → ℕ
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.eq_symm_apply : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) {x : M₂}
  {y : M₁}, y = f.symm x ↔ f y = x
-- Init.Data.Int.Order
Int.neg_add_lt_of_lt_add : ∀ {a b c : ℤ}, a < b + c → -b + a < c
-- Mathlib.Logic.Equiv.Bool
Equiv.boolNot_symm_apply : ∀ (a : Bool), (Equiv.symm Equiv.boolNot) a = !a
-- Init.Data.Array.Lemmas
Array.extract_congr : ∀ {α : Type u_1} {start start' stop stop' : ℕ} {xs ys : Array α},
  xs = ys → start = start' → stop = stop' → xs.extract start stop = ys.extract start' stop'
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_intCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIocMod hp a (b + ↑m * p) = toIocMod hp a b
-- Lean.Parser.Types
Lean.Parser.FirstTokens.optTokens : List Lean.Parser.Token → Lean.Parser.FirstTokens
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.term : Lean.Term → Aesop.Frontend.Feature
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.div_closedBall : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), s / Metric.closedBall x δ = x⁻¹ • Metric.cthickening δ s
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- `weierstrassPExcept l₀` is differentiable on non-lattice points and `l₀`.  -/
PeriodPair.differentiableOn_weierstrassPExcept : ∀ (L : PeriodPair) (l₀ : ℂ), DifferentiableOn ℂ (L.weierstrassPExcept l₀) (↑L.lattice \ {l₀})ᶜ