mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.copy.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β] (f : InfTopHom α β)
  (f' : α → β) (h : f' = ⇑f), f.copy f' h = { toInfHom := f.copy f' h, map_top' := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.pp : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.GoalM Lean.MessageData
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair_map_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A)
  {sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B}
  {sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B},
  (CategoryTheory.Limits.reflexivePair f g s sl sr).map CategoryTheory.Limits.WalkingReflexivePair.Hom.left = f
-- Init.Data.SInt.Lemmas
Int32.toBitVec_ofIntTruncate : ∀ {n : ℤ}, Int32.minValue.toInt ≤ n → n ≤ Int32.maxValue.toInt → (Int32.ofIntClamp n).toBitVec = BitVec.ofInt 32 n
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithBot.coe_biInf : ∀ {ι : Type u_5} {s : Set ι} {α : Type u_6} [inst : CompleteLattice α] (f : ι → α), ↑(⨅ i ∈ s, f i) = ⨅ i ∈ s, ↑(f i)
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Relation between the logarithmic counting functions of `f` and of `f⁻¹`.
 -/
ValueDistribution.logCounting_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {f : 𝕜 → 𝕜},
  ValueDistribution.logCounting f⁻¹ ⊤ = ValueDistribution.logCounting f 0
-- Mathlib.Data.Stream.Init
Stream'.even_tail : ∀ {α : Type u} (s : Stream' α), s.tail.even = s.odd
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_le_iff : ∀ {α : Type u_1} {G : SimpleGraph α} {k : ℕ∞}, G.ediam ≤ k ↔ ∀ (u v : α), G.edist u v ≤ k
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.map_comp_map : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  {I : Type u_5} [inst_2 : AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [inst_3 : M.Normal] [inst_4 : O.Normal]
  (f : G →+ H) (g : H →+ I) (hf : N ≤ AddSubgroup.comap f M) (hg : M ≤ AddSubgroup.comap g O)
  (hgf : optParam (N ≤ AddSubgroup.comap (g.comp f) O) ⋯),
  (QuotientAddGroup.map M O g hg).comp (QuotientAddGroup.map N M f hf) = QuotientAddGroup.map N O (g.comp f) hgf
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
/-- `arg` returns values in the range $(-π, π]$, such that for `x ≠ 0`,
`sin (arg x) = x.im / x.abs` and `cos (arg x) = x.re / x.abs`,
`arg 0` defaults to `0`  -/
Complex.arg : ℂ → ℝ
-- Mathlib.Algebra.Module.Basic
Set.indicator_smul_apply : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SMulZeroClass R M] (s : Set α) (r : α → R)
  (f : α → M) (a : α), s.indicator (fun a => r a • f a) a = r a • s.indicator f a
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singletonAddMonoidHom_apply : ∀ {α : Type u_2} [inst : AddZeroClass α] (a : α), Set.singletonAddMonoidHom a = {a}
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.map_const : ∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (b : β), PMF.map (Function.const α b) p = PMF.pure b
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_le_comap_iff_of_surjective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Surjective ⇑f →
    ∀ {S T : L.Substructure N},
      FirstOrder.Language.Substructure.comap f S ≤ FirstOrder.Language.Substructure.comap f T ↔ S ≤ T
-- Mathlib.Analysis.Calculus.FDeriv.Partial
/-- If bivariate `f : E₁ → E₂ → F` has partial derivatives `f₁` and `f₂` in a neighbourhood of
`u : E₁ × E₂` and if they are continuous there then the uncurried function `↿f` is strictly
differentiable at `u` with its derivative mapping `z` to `f₁ u.1 u.2 z.1 + f₂ u.1 u.2 z.2`.  -/
hasStrictFDerivAt_uncurry_coprod : ∀ {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : NormedAddCommGroup E₂]
  [inst_4 : NormedSpace 𝕜 E₂] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [IsRCLikeNormedField 𝕜]
  {u : E₁ × E₂} {f : E₁ → E₂ → F} {f₁ : E₁ → E₂ → E₁ →L[𝕜] F} {f₂ : E₁ → E₂ → E₂ →L[𝕜] F},
  (∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f x v.2) (↿f₁ v) v.1) →
    (∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f v.1 x) (↿f₂ v) v.2) →
      ContinuousAt (↿f₁) u → ContinuousAt (↿f₂) u → HasStrictFDerivAt (↿f) ((↿f₁ u).coprod (↿f₂ u)) u
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.instIsContinuousCompOverForgetForgetTopologyProetaleTopology : ∀ (S : AlgebraicGeometry.Scheme),
  ((AlgebraicGeometry.Scheme.ProEt.forget S).comp (CategoryTheory.Over.forget S)).IsContinuous
    (AlgebraicGeometry.Scheme.ProEt.topology S) AlgebraicGeometry.Scheme.proetaleTopology
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.modifyGet_EStateM : ∀ {ε σ α : Type u_1} {f : σ → α × σ}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))},
  ⦃fun s =>
    have t := f s;
    Q.1 t.1 t.2⦄
    MonadStateOf.modifyGet f ⦃Q⦄
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_eq_none : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {a : α}, m.contains a = false → Std.DHashMap.Internal.Raw₀.Const.get? m a = none
-- Mathlib.Condensed.Discrete.Colimit
/-- The restriction of a finite-product-preserving presheaf `F` on `Profinite` to the category of
finite sets is isomorphic to `finYoneda F`.
 -/
LightCondensed.isoFinYoneda : (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] → FintypeCat.toLightProfinite.op.comp F ≅ LightCondensed.finYoneda F
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
_private.Std.Tactic.BVDecide.LRAT.Internal.Assignment.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_1 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_1 ()
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasAdditiveReduction.not_hasMultiplicativeReduction : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K},
  WeierstrassCurve.HasAdditiveReduction R W → ¬WeierstrassCurve.HasMultiplicativeReduction R W
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.sOppSide_excenter_point_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {i : Fin (n + 1)},
      (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SOppSide (s.excenter signs) (s.points i) ↔
        s.excenterWeights signs i < 0
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.fold_filterWithPostcondition : ∀ {ps : Std.Do.PostShape} {α β δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Std.Do.WPMonad n ps]
  [inst_5 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n]
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {g : δ → β → δ} {init : δ} {it : Std.Iter β}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let __do_lift ← (f b).run
          pure (if __do_lift.down = true then g d b else d))
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.Iter.filterWithPostcondition f it) ⦃Q⦄
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.map_altitude_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)),
  AffineSubspace.map S.subtype ((s.restrict S hS).altitude i) = s.altitude i
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.codChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (self : Manifold.LocalPresentationAt I J n f x P), self.codChart ∈ IsManifold.maximalAtlas J n N
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_inv : ∀ {G : Type u_4} [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [inst_2 : MeasurableInv G],
  (MeasurableEquiv.inv G).symm = MeasurableEquiv.inv G
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.single_zero : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α), lp.single p i 0 = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ext_iff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x y : MonoidAlgebra R M}, x = y ↔ x.coeff = y.coeff
-- Mathlib.Data.FP.Basic
FP.nextUp : [C : FP.FloatCfg] → FP.Float → FP.Float
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- `A : Matrix V V α` is qualified as an "adjacency matrix" if
(1) every entry of `A` is `0` or `1`,
(2) `A` is symmetric,
(3) every diagonal entry of `A` is `0`.  -/
Matrix.IsAdjMatrix : {α : Type u_1} → {V : Type u_2} → [Zero α] → [One α] → Matrix V V α → Prop
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.le_pow_of_le_ramificationIdx'`. -/
Ideal.le_pow_of_le_ramificationIdx : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  {n : ℕ}, n ≤ p.ramificationIdx' P → Ideal.map (algebraMap R S) p ≤ P ^ n
-- Lean.Parser.Basic
Lean.Syntax.foldArgsM : {m : Type u_1 → Type u_2} → [Monad m] → {β : Type u_1} → Lean.Syntax → (Lean.Syntax → β → m β) → β → m β
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The direction of the affine span of a family indexed by a
`Fintype` is finite-dimensional.  -/
finiteDimensional_direction_affineSpan_range : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [Finite ι] (p : ι → P),
  FiniteDimensional k ↥(affineSpan k (Set.range p)).direction
-- Lean.Compiler.LCNF.Basic
/-- Full, impure, application of a function.
 -/
Lean.Compiler.LCNF.LetValue.fap : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Name →
    Array (Lean.Compiler.LCNF.Arg pu) →
      autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_13 →
        Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Data.WSeq.Defs
/-- Get the length of `s` (if it is finite and completes in finite time).  -/
Stream'.WSeq.length : {α : Type u} → Stream'.WSeq α → Computation ℕ
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.ObjectProperty.fullSubcategoryCongr_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P'),
  (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).counitIso =
    CategoryTheory.Iso.refl ((CategoryTheory.ObjectProperty.ιOfLE ⋯).comp (CategoryTheory.ObjectProperty.ιOfLE ⋯))
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.mk.sizeOf_spec : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] [inst_1 : SizeOf X] [inst_2 : SizeOf G]
  (toPartialEquiv : PartialEquiv X X)
  (isDecompOn' : ∃ S, Equidecomp.IsDecompOn (↑toPartialEquiv) toPartialEquiv.source S),
  sizeOf { toPartialEquiv := toPartialEquiv, isDecompOn' := isDecompOn' } =
    1 + sizeOf toPartialEquiv + sizeOf isDecompOn'
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Fix a sequence `i : ℕ → β`. Given a function `α → β`, its `n`-th approximation
by simple functions is defined so that in case `β = ℝ≥0∞` it sends each `a` to the supremum
of the set `{i k | k ≤ n ∧ i k ≤ f a}`, see `approx_apply` and `iSup_approx_apply` for details.  -/
MeasureTheory.SimpleFunc.approx : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : SemilatticeSup β] → [OrderBot β] → [Zero β] → (ℕ → β) → (α → β) → ℕ → MeasureTheory.SimpleFunc α β
-- Mathlib.Analysis.Calculus.FDeriv.Prod
/-- A variant of `hasFDerivWithinAt_finCons` where the derivative variables are free on the RHS
instead.  -/
hasFDerivWithinAt_finCons' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ},
  HasFDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') s x ↔
    HasFDerivWithinAt φ φ' s x ∧ HasFDerivWithinAt φs φs' s x
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
/-- A function is `C^(n + 1)` on an open domain if and only if it is
differentiable there, and its derivative (formulated with `deriv`) is `C^n`.  -/
contDiffOn_succ_iff_deriv_of_isOpen : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜},
  IsOpen s →
    (ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (deriv f) s)
-- Lean.Data.Lsp.Extra
Lean.Lsp.ModuleHierarchyOptions.noConfusionType : Sort v✝ → Lean.Lsp.ModuleHierarchyOptions → Lean.Lsp.ModuleHierarchyOptions → Sort v✝
-- Mathlib.Data.Nat.Count
Nat.lt_of_count_lt_count : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {a b : ℕ}, Nat.count p a < Nat.count p b → a < b
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonWaitForILeans : Lean.ToJson Lean.Lsp.WaitForILeans
-- Mathlib.Algebra.Group.Basic
div_eq_div_iff_comm : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b c : α) {d : α}, a / b = c / d ↔ b / a = d / c
-- Mathlib.Topology.Separation.Regular
/-- Given a subbasis `s`, it is enough to check the condition of regularity for complements of sets
in `s`.  -/
regularSpace_generateFrom : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (Set X)},
  inst = TopologicalSpace.generateFrom s → (RegularSpace X ↔ ∀ t ∈ s, ∀ a ∈ t, Disjoint (nhdsSet tᶜ) (nhds a))
-- Mathlib.Algebra.Group.WithOne.Basic
AddEquiv.withZeroCongr_refl : ∀ {α : Type u} [inst : Add α], (AddEquiv.refl α).withZeroCongr = AddEquiv.refl (WithZero α)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_empty : ∀ {α : Type u} (h : ∅.Finite), h.toFinset = ∅
-- Mathlib.Data.Real.Basic
Real.instIntCast : IntCast ℝ
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.innerContent_exists_compact : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) {U : TopologicalSpace.Opens G},
  μ.innerContent U ≠ ⊤ → ∀ {ε : NNReal}, ε ≠ 0 → ∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ K + ↑ε
-- Init.Data.String.PosRaw
/-- Move the position `p` back by `n` bytes. This is not an `HSub` instance because it should be a
relatively rare operation, so we use a name to make accidental use less likely. To remove the size
of a character `c` or string `s` from a raw position `p`, you can use `p - c` resp. `p - s`.

This should be seen as the inverse of an "advance" or "skip".

See also `Pos.Raw.unoffsetBy`, which turns absolute positions into relative positions.
 -/
String.Pos.Raw.decreaseBy : String.Pos.Raw → ℕ → String.Pos.Raw
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.linear_iff : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (F : CategoryTheory.Functor C D),
  CategoryTheory.Functor.Linear R F ↔
    ∀ (X : C) (r : R), F.map (r • CategoryTheory.CategoryStruct.id X) = r • CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_add_right_eball`. -/
EMetric.preimage_add_right_ball : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ENNReal),
  (fun x => x + a) ⁻¹' Metric.eball b r = Metric.eball (b - a) r
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_mul_nat : ∀ {n : ℕ}, n ≠ 0 → Cardinal.aleph0 * ↑n = Cardinal.aleph0
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- **Conditional summation**, for ordered types `β` such that closed intervals `[x, y]` are
finite: this corresponds to limits of finite sums over larger and larger intervals.  -/
SummationFilter.conditional : (β : Type u_2) → [inst : Preorder β] → [LocallyFiniteOrder β] → SummationFilter β
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Error.other.inj : ∀ {s s_1 : String}, Std.Internal.Parsec.Error.other s = Std.Internal.Parsec.Error.other s_1 → s = s_1
-- Mathlib.LinearAlgebra.Complex.Module
skewAdjoint.I_smul_neg_I : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (a : ↥(skewAdjoint A)), Complex.I • ↑(skewAdjoint.negISMul a) = ↑a
-- Init.System.ST
/-- A restricted version of `IO` in which mutable state is the only side effect.

It is possible to run `ST` computations in a non-monadic context using `runST`.
 -/
ST : Type → Type → Type
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.from_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsZero X) (f : Y ⟶ X),
  h.from_ Y = f
-- Init.Data.SInt.Lemmas
USize.toISize_ofNatLT : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatLT n hn).toISize = ISize.ofNat n
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
/-- The complement of a strongly regular graph is strongly regular.  -/
SimpleGraph.IsSRGWith.compl : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V], G.IsSRGWith n k ℓ μ → Gᶜ.IsSRGWith n (n - k - 1) (n - (2 * k - μ) - 2) (n - (2 * k - ℓ))
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
tateComplexFunctor_map : ∀ (R G : Type u) [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] {X Y : Rep.{u, u, u} R G} (φ : X ⟶ Y),
  (tateComplexFunctor R G).map φ = tateComplex.map φ
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The identity transformation induces the identity endofunctor on the category of coalgebras.  -/
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans (CategoryTheory.CategoryStruct.id F) ≅
        CategoryTheory.Functor.id (CategoryTheory.Endofunctor.Coalgebra F)
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isStrictlyGE_mapHomologicalComplex_obj_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.Faithful]
  [inst_5 : F.PreservesZeroMorphisms] (n : ℤ),
  CochainComplex.IsStrictlyGE ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) n ↔ K.IsStrictlyGE n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_one_of_mul_le_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulRightReflectLE α] {a b : α}, a * b ≤ b → a ≤ 1
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be an integral domain and `f, g₁, g₂ : R[X]`. Let `g₁` and `g₂` be monic and coprime.
Then the representation of `f / (g₁ * g₂)` as `q + r₁ / g₁ + r₂ / g₂` for `q r₁ r₂ : R[X]` and
`degree rᵢ < degree gᵢ` is unique, where the equality is taken in a field `K` containing `R[X]`.
See `div_eq_quo_add_rem_div_add_rem_div` for the existence of such a representation.  -/
Polynomial.quo_add_rem_div_add_rem_div_unique : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra (Polynomial R) K]
  [FaithfulSMul (Polynomial R) K] {g₁ g₂ : Polynomial R},
  g₁.Monic →
    g₂.Monic →
      IsCoprime g₁ g₂ →
        ∀ {q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : Polynomial R},
          r₁₁.degree < g₁.degree →
            r₁₂.degree < g₁.degree →
              r₂₁.degree < g₂.degree →
                r₂₂.degree < g₂.degree →
                  ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂ → q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂
-- Mathlib.RingTheory.LocalProperties.Exactness
IsLocalization.Away.map.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (Q : Type u_4) [inst_4 : CommSemiring Q] [inst_5 : Algebra P Q] (f f_1 : R →+* P)
  (e_f : f = f_1) (r r_1 : R) (e_r : r = r_1) [inst_6 : IsLocalization.Away r S] [inst_7 : IsLocalization.Away (f r) Q],
  IsLocalization.Away.map S Q f r = IsLocalization.Away.map S Q f_1 r_1
-- Mathlib.Data.List.Sublists
List.sublists.eq_1 : ∀ {α : Type u_1} (l : List α), l.sublists = List.foldr (fun a acc => List.flatMap (fun x => [x, a :: x]) acc) [[]] l
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.mk'.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {x : AddCommGroup α} {x_1 : Preorder α} {x_2 : AddCommGroup β} {x_3 : PartialOrder β}
  (f : α ≃ β) (hf : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b) (map_mul : ∀ (a b : α), f (a + b) = f a + f b),
  OrderAddMonoidIso.mk' f hf map_mul = { toAddEquiv := AddEquiv.mk' f map_mul, map_le_map_iff' := ⋯ }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.minEntryD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {fallback : (a : α) × β a}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minEntryD fallback = t₂.minEntryD fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.map_polynomial : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] (f : R →+* S),
  (W'.map f).polynomial = (MvPolynomial.map f) W'.polynomial
-- Mathlib.FieldTheory.AlgebraicClosure
/-- The *relative algebraic closure* of a field `F` in a field extension `E`,
also called the *maximal algebraic subextension* of `E / F`,
is defined to be the subalgebra `integralClosure F E`
upgraded to an intermediate field (since `F` and `E` are both fields).
This is exactly the intermediate field of `E / F` consisting of all integral/algebraic elements.
 -/
algebraicClosure : (F : Type u_1) → (E : Type u_2) → [inst : Field F] → [inst_1 : Field E] → [inst_2 : Algebra F E] → IntermediateField F E