mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
FundamentalGroup.mul_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {p q : FundamentalGroup X x},
  p * q = Path.Homotopic.Quotient.trans q p
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.lift_π : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {P : C} (p : (b : J) → P ⟶ f b) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift p) (CategoryTheory.Limits.biproduct.π f j) =
    p j
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.exists_mono : ∀ {σs : List (Type u)} {α : Sort u_1} {Φ Ψ : α → Std.Do.SPred σs}, (∀ (a : α), Φ a ⊢ₛ Ψ a) → (∃ a, Φ a) ⊢ₛ ∃ a, Ψ a
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is polynomial on a set `s`, so are its successive Fréchet derivative.  -/
CPolynomialOn.iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, CPolynomialOn 𝕜 f s → ∀ (n : ℕ), CPolynomialOn 𝕜 (iteratedFDeriv 𝕜 n f) s
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The sum of measurable functions is measurable.  -/
Measurable.tsum' : ∀ {X : Type u_6} {E : Type u_7} {ι : Type u_8} [inst : MeasurableSpace X] [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [inst_4 : MeasurableSpace E] [BorelSpace E]
  [MeasurableAdd₂ E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {f : ι → X → E},
  (∀ (i : ι), Measurable (f i)) → Measurable (∑'[L] (i : ι), f i)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_div_flip : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [MulLeftMono α] {a b : α}, a / b ≤ b / a ↔ a ≤ b
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_X_pow_assoc : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] (m n : ℕ),
  x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The underlying family of polynomials of an induction object.  -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.val : {R : Type u_2} → [inst : CommRing R] → {n : ℕ} → ChevalleyThm.PolynomialC.InductionObj✝ R n → Fin n → Polynomial R
-- Mathlib.Condensed.Equivalence
Condensed.isSheafProfinite : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] (X : Condensed A)
  [∀ (Y : CompHausᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow Y profiniteToCompHaus.op) A],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Profinite) (profiniteToCompHaus.op.comp X.obj)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat.injEq : ∀ (e : Lean.Expr) (natStructId : ℕ) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) (e_1 : Lean.Expr)
  (natStructId_1 : ℕ) (lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat e natStructId lhs rhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat e_1 natStructId_1 lhs_1 rhs_1) =
    (e = e_1 ∧ natStructId = natStructId_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- The group of affine isometries of a `NormedAddTorsor`, `P`.  -/
AffineIsometryEquiv.instGroup : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] →
            [inst_3 : PseudoMetricSpace P] → [inst_4 : NormedAddTorsor V P] → Group (P ≃ᵃⁱ[𝕜] P)
-- Mathlib.RingTheory.FormalGroup.Basic
/-- The constant coefficient of the formal group law is zero.  -/
FormalGroup.zero_constantCoeff : ∀ {R : Type u_1} [inst : CommRing R] (self : FormalGroup R), MvPowerSeries.constantCoeff self.toPowerSeries = 0
-- Mathlib.Analysis.RCLike.Extend
/-- Extend `fr : Dual ℝ F` to `Dual 𝕜 F` in a way that will also be continuous and have its norm
(as a continuous linear map) equal to `‖fr‖` when `fr` is itself continuous on a normed space.  -/
Module.Dual.extendRCLike : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {F : Type u_2} →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module ℝ F] → [inst_3 : Module 𝕜 F] → [IsScalarTower ℝ 𝕜 F] → Module.Dual ℝ F → Module.Dual 𝕜 F
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter!_eq_self_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      k ∈ t → (f (t.get? k)).isSome = true → (Std.DTreeMap.Internal.Impl.alter! k f t).size = t.size
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.ofHom.eq_1 : ∀ {X Y : Type u} [inst : Group X] [inst_1 : Group Y] (f : X →* Y),
  GrpCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- The natural map from `n`-cocycles to `n`th group cohomology for a `k`-linear
`G`-representation `A`.  -/
groupCohomology.π : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → (n : ℕ) → groupCohomology.cocycles A n ⟶ groupCohomology A n
-- Mathlib.Algebra.Group.Torsion
pow_left_inj : ∀ {M : Type u_1} [inst : Monoid M] [IsMulTorsionFree M] {n : ℕ} {a b : M}, n ≠ 0 → (a ^ n = b ^ n ↔ a = b)
-- Mathlib.Analysis.Distribution.DerivNotation
ContinuousLineDeriv.continuous_lineDerivOp : ∀ {V : Type u} {E : Type v} {F : outParam (Type w)} {inst : TopologicalSpace E} {inst_1 : TopologicalSpace F}
  {inst_2 : LineDeriv V E F} [self : ContinuousLineDeriv V E F] (v : V), Continuous (LineDeriv.lineDerivOp v)
-- Std.Time.DateTime.PlainDateTime
/-- Adds a `Month.Offset` to a `PlainDateTime`, rolling over excess days to the following month if needed.
 -/
Std.Time.PlainDateTime.addYearsRollOver : Std.Time.PlainDateTime → Std.Time.Year.Offset → Std.Time.PlainDateTime
-- Init.Data.Nat.Basic
Nat.instLawfulIdentityHAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.Data.Finsupp.ToDFinsupp
Finsupp.toDFinsupp_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (f g : ι →₀ M), (f + g).toDFinsupp = f.toDFinsupp + g.toDFinsupp
-- Mathlib.Algebra.Category.Grp.Adjunctions
MonCat.val_units_map_hom_apply : ∀ {X Y : MonCat} (f : X ⟶ Y) (u : (↑X)ˣ), ↑((GrpCat.Hom.hom (MonCat.units.map f)) u) = (MonCat.Hom.hom f) ↑u
-- Mathlib.Analysis.LocallyConvex.Montel
ContinuousLinearEquiv.toCompactConvergenceCLM_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : IsTopologicalAddGroup E] [inst_6 : ContinuousSMul 𝕜₁ E] [inst_7 : AddCommGroup F] [inst_8 : Module 𝕜₂ F]
  [inst_9 : TopologicalSpace F] [inst_10 : IsTopologicalAddGroup F] [inst_11 : ContinuousSMul 𝕜₂ F]
  [inst_12 : T1Space E] [inst_13 : MontelSpace 𝕜₁ E] (f : E →SL[σ] F) (x : E),
  ((ContinuousLinearEquiv.toCompactConvergenceCLM σ E F) f) x = f x
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL_eq_balanceLErase : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size},
  Std.DTreeMap.Internal.Impl.balanceL k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balanceLErase k v l r hlb hrb ⋯
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.isClosed_union_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X},
  SeparatedNhds s t → (IsClosed (s ∪ t) ↔ IsClosed s ∧ IsClosed t)
-- Mathlib.CategoryTheory.Galois.Basic
/-- Definition of a (Pre)Galois category. Lenstra, Def 3.1, (G1)-(G3)  -/
CategoryTheory.PreGaloisCategory : (C : Type u₁) → [CategoryTheory.Category.{u₂, u₁} C] → Prop
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.Xzero_eq_X : ∀ {R : Type u_1} [inst : CommRing R] (F : FormalGroup R), F.Xzero = PowerSeries.X
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.endHom_toMatrix : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {P : Type u_5} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  [inst_7 : Module S P] [inst_8 : IsScalarTower R S P] {α : M →ₗ[R] P} (ibcM : IsBaseChange S α) {ι : Type u_7}
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι] (b : Module.Basis ι R M) (f : M →ₗ[R] M),
  (LinearMap.toMatrix (IsBaseChange.basis b ibcM) (IsBaseChange.basis b ibcM)) (ibcM.endHom f) =
    ((LinearMap.toMatrix b b) f).map ⇑(algebraMap R S)
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.Exists.eq_def : ∀ {α : Type u_1} (x : ℕ) (x_1 : (Fin x → α) → Prop),
  FinVec.Exists x_1 =
    match x, x_1 with
    | 0, P => P ![]
    | n.succ, P => ∃ x, FinVec.Exists fun v => P (Matrix.vecCons x v)
-- Mathlib.Analysis.Complex.RemovableSingularity
/-- **Removable singularity** theorem: if a function `f : ℂ → E` is complex differentiable and
bounded on a punctured neighborhood of `c`, then `f` has a limit at `c`.  -/
Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ},
  (∀ᶠ (z : ℂ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℂ f z) →
    (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhdsWithin c {c}ᶜ) fun z => ‖f z - f c‖) →
      Filter.Tendsto f (nhdsWithin c {c}ᶜ) (nhds ((nhdsWithin c {c}ᶜ).limUnder f))
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
_private.Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation.0.ValueDistribution.Cartan.integral_norm_cartanKernel_eq : ∀ (f : ℂ → ℂ) (R β : ℝ),
  ∫ (α : ℝ) in Set.Ioc 0 (2 * Real.pi), ‖ValueDistribution.Cartan.cartanKernel f R α β‖ =
    (2 * ∫ (α : ℝ) in Set.Ioc 0 (2 * Real.pi), (ValueDistribution.Cartan.cartanKernel f R α β)⁺) -
      2 * Real.pi * ‖f (circleMap 0 R β)‖.posLog
-- Mathlib.Analysis.LocallyConvex.AbsConvex
nhds_hasBasis_absConvex : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [LocallyConvexSpace 𝕜 E] [ContinuousSMul 𝕜 E],
  (nhds 0).HasBasis (fun s => s ∈ nhds 0 ∧ AbsConvex 𝕜 s) id
-- Init.Data.String.Lemmas.Slice
_private.Init.Data.String.Lemmas.Slice.0.String.Slice.beq.eq_1 : ∀ (s1 s2 : String.Slice),
  s1.beq s2 =
    if h : s1.utf8ByteSize = s2.utf8ByteSize then
      have h1 := ⋯;
      have h2 := ⋯;
      String.Slice.Pattern.Internal.memcmpSlice s1 s2 s1.startPos.offset s2.startPos.offset s1.rawEndPos h1 h2
    else false
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. `lowerBound? k` retrieves the key-value pair of the largest key
smaller than or equal to `k`, if it exists.
 -/
RBTree.RBMap.lowerBound? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → α → Option (α × β)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞},
  UniqueDiffOn 𝕜 s →
    (ContDiffOn 𝕜 (n + 1) f s ↔
      (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ∃ f', ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_indicator_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) (s : Set α),
  ∫⁻ (a : α), s.indicator f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.div_inv : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α] [inst_1 : Neg β],
  Function.Antiperiodic f c → ∀ {a : α}, a ≠ 0 → Function.Antiperiodic (fun x => f (x / a)) (c * a)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- **Alias** of the forward direction of `MeasureTheory.IntegrableAtFilter.inf_ae_iff`. -/
MeasureTheory.IntegrableAtFilter.of_inf_ae : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l : Filter α},
  MeasureTheory.IntegrableAtFilter f (l ⊓ MeasureTheory.ae μ) μ → MeasureTheory.IntegrableAtFilter f l μ
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.prod.eq_1 : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] (x_2 : Fin 0 → α), FinVec.prod x_2 = 1
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv_one : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), RegularExpression.deriv 1 a = 0
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.asympBound_def : ∀ (g : ℝ → ℝ) {α : Type u_2} [inst : Fintype α] (a b : α → ℝ) {n : ℕ},
  AkraBazziRecurrence.asympBound g a b n =
    ↑n ^ AkraBazziRecurrence.p a b + AkraBazziRecurrence.sumTransform (AkraBazziRecurrence.p a b) g 0 n
-- Mathlib.Computability.Language
/-- The product of two languages `l` and `m` is the language made of the strings `x ++ y` where
`x ∈ l` and `y ∈ m`.  -/
Language.instMul : {α : Type u_1} → Mul (Language α)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.measurableSet_paramSet : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasurableSet (NumberField.mixedEmbedding.fundamentalCone.paramSet K)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.instFaithfulFunctorWhiskeringLeftFunctor' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W], (CategoryTheory.Localization.whiskeringLeftFunctor' L W E).Faithful
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
indicator_le_thickenedIndicator : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α),
  (E.indicator fun x => 1) ≤ ⇑(thickenedIndicator δ_pos E)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.zero : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3}, PowerSeries.HasSubst 0
-- Mathlib.Analysis.Normed.Group.Basic
NormedAddCommGroup.tendsto_nhds_nhds : ∀ {E : Type u_5} {F : Type u_6} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] {f : E → F}
  {x : E} {y : F}, Filter.Tendsto f (nhds x) (nhds y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' - x‖ < δ → ‖f x' - y‖ < ε
-- Mathlib.RingTheory.Noetherian.Basic
/-- A submodule contained in an noetherian submodule is FG.  -/
Submodule.FG.of_le_of_isNoetherian : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S T : Submodule R M}
  [IsNoetherian R ↥T], S ≤ T → S.FG
-- Mathlib.Order.Filter.Pointwise
/-- `1 : Filter α` is defined as the filter of sets containing `1 : α` in scope `Pointwise`.  -/
Filter.instOne : {α : Type u_2} → [One α] → One (Filter α)
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_eval_one_sub : ∀ (n : ℕ) (x : ℚ),
  Polynomial.eval (1 - x) (Polynomial.bernoulli n) = (-1) ^ n * Polynomial.eval x (Polynomial.bernoulli n)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.raised_iff : ∀ {n m : ℕ}, Ordnode.Raised n m ↔ n ≤ m ∧ m ≤ n + 1
-- Mathlib.Data.Set.SMulAntidiagonal
Set.VAddAntidiagonal.finite_of_finite : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} [inst : VAdd G P] [IsLeftCancelVAdd G P],
  s.Finite → ∀ (t : Set P) (p : P), (s.vaddAntidiagonal t p).Finite
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.divX_hom.eq_1 : ∀ {R : Type u} [inst : Semiring R], Polynomial.divX_hom = { toFun := Polynomial.divX, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Tactic.Hint
/-- Return the list of registered hint tactics.  -/
Mathlib.Tactic.Hint.getHints : Lean.CoreM (List (ℕ × Lean.TSyntax `tactic))
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- A presheaf valued in a category `A` with arbitrary products can be extended to the category of
formal coproducts.  -/
CategoryTheory.Limits.FormalCoproduct.evalOp : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : Type u₁) →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        [CategoryTheory.Limits.HasProducts A] →
          CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A)
            (CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ A)
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_comp_equiv_apply_eq_self : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : ExpChar L p]
  [inst_6 : PerfectRing L p] [inst_7 : IsPerfectClosure i p] [inst_8 : PerfectRing M p] [inst_9 : IsPerfectClosure j p]
  (x : L), (IsPerfectClosure.equiv j i p) ((IsPerfectClosure.equiv i j p) x) = x
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.nonTorsionWeight_of : ∀ {M : Type u_2} {σ : Type u_3} [inst : AddCommMonoid M] {w : σ → M} [IsAddTorsionFree M],
  (∀ (i : σ), w i ≠ 0) → MvPolynomial.NonTorsionWeight w
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_univ_singleton : ∀ {G : Type u_1} [inst : Group G] {g : G}, Subgroup.IsComplement Set.univ {g}
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.SpecialLinear.single.congr_simp : ∀ {n : Type u_1} {R : Type u₂} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i i_1 : n)
  (e_i : i = i_1) (j j_1 : n) (e_j : j = j_1) (h : i ≠ j),
  LieAlgebra.SpecialLinear.single i j h = LieAlgebra.SpecialLinear.single i_1 j_1 ⋯
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.iterator_ofIterM : ∀ {m : Type u_1 → Type u_2} {β α : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β),
  (Std.BundledIterM.ofIterM it).iterator = it
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.R.intro : ∀ {K : Type u} [inst : CommRing K] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (n : ℕ) (x : K),
  PerfectClosure.R K p (n, x) (n + 1, (frobenius K p) x)
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_iff_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, s ∈ nhds x → (ContinuousWithinAt f s x ↔ ContinuousAt f x)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.ofTruncated_edge : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : SSet.Truncated.Edge x₀ x₁),
  (SSet.Edge.ofTruncated e).edge = e.edge
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- **Alias** of `isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_le`.

---

**Prokhorov theorem**: Given a sequence of compact sets `Kₙ` and a sequence `uₙ` tending to
zero, the finite measures of mass `C` giving mass at most `uₙ` to the complement of `Kₙ` form a
compact set.  -/
isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le : ∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal),
  Filter.Tendsto u Filter.atTop (nhds 0) →
    (∀ (n : ℕ), IsCompact (K n)) → NormalSpace E ∨ Monotone K → IsCompact {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.notMem_support_iff : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, n ∉ p.support ↔ p.coeff n = 0
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has bounded variation and is left-continuous at a point, then the variation on
small closed intervals to the left of this point tends to `0`.  -/
BoundedVariationOn.tendsto_eVariationOn_Icc_zero_left : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α},
  BoundedVariationOn f s →
    ∀ {x : α},
      ContinuousWithinAt f (s ∩ Set.Iic x) x →
        Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Icc y x)) (nhdsWithin x s) (nhds 0)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_eq_zero_iff : ∀ {θ : Real.Angle}, θ.sin = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.instCoeFun : {η : Type u_5} → {α : Type u_6} → {ι : Type u_7} → CoeFun (Combinatorics.Subspace η α ι) fun x => (η → α) → ι → α
-- Init.Data.UInt.Bitwise
UInt8.toBitVec_shiftLeft : ∀ (a b : UInt8), (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 8)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.instCommRing : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type u_3} → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → {S : Submonoid R} → CommRing (LocalizedModule S A)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_ofList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)}, (Std.DHashMap.Raw.ofList l).isEmpty = l.isEmpty
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_units_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} (n m : ℤ) (k : Rˣ)
  (z : CochainComplex.HomComplex.Cochain F G n),
  CochainComplex.HomComplex.δ n m (k • z) = k • CochainComplex.HomComplex.δ n m z
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- Flipping a pushout cocone twice gives an isomorphic cocone.  -/
CategoryTheory.Limits.PushoutCocone.flipFlipIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → {f : X ⟶ Y} → {g : X ⟶ Z} → (t : CategoryTheory.Limits.PushoutCocone f g) → t.flip.flip ≅ t
-- Lean.MetavarContext
Lean.MetavarContext.MkBindingM : Type → Type
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- Let `D` be the decomposition field of `P` in `L/K`. Let `𝓟D` be a prime ideal of `D` below `P`,
then the ramification index of `𝓟D` in `L` is equal to the ramification index of `p` in `L`.
 -/
IsDecompositionField.ramificationIdxIn_eq : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [inst_7 : Algebra A K] [IsFractionRing A K] [inst_9 : Algebra A L] [IsScalarTower A K L] [inst_11 : Algebra B L]
  [IsScalarTower A B L] [IsFractionRing B L] [inst_14 : MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L]
  (D : Type u_5) (𝓞D : Type u_6) [inst_16 : Field D] [inst_17 : Algebra D L] [IsDecompositionField K L P D]
  [inst_19 : CommRing 𝓞D] [inst_20 : Algebra 𝓞D D] [IsFractionRing 𝓞D D] [inst_22 : Algebra 𝓞D B]
  [inst_23 : Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D]
  [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B]
  [inst_31 : Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B] [IsDedekindDomain 𝓞D] [𝓟D.LiesOver p]
  [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal],
  p ≠ ⊥ → 𝓟D.ramificationIdxIn B = p.ramificationIdxIn B
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.ExtTreeMap.map f t},
  (Std.ExtTreeMap.map f t)[k] = f k t[k]