mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.divMod.congr_simp : ∀ {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] (c c_1 : FractionalIdeal (nonZeroDivisors R) K),
  c = c_1 →
    ∀ (b b_1 : FractionalIdeal (nonZeroDivisors R) K),
      b = b_1 → ∀ (a a_1 : FractionalIdeal (nonZeroDivisors R) K), a = a_1 → c.divMod b a = c_1.divMod b_1 a_1
-- Lean.Meta.PProdN
_private.Lean.Meta.PProdN.0.Lean.Meta.PProdN.reduceProjs.reduce : Lean.Expr → ℕ → Lean.MetaM Lean.TransformStep
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.CommSemiRingCat.Hom.mk.injEq : ∀ {R S : CommSemiRingCat} (hom' hom'_1 : ↑R →+* ↑S), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.inr_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q), CategoryTheory.CategoryStruct.comp self.inr self.fst = 0
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.relabel_atom : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {idx : ℕ} {a : β} {aig : Std.Sat.AIG α} {r : α → β} {hidx : idx < (Std.Sat.AIG.relabel r aig).decls.size},
  (Std.Sat.AIG.relabel r aig).decls[idx] = Std.Sat.AIG.Decl.atom a →
    ∃ x, aig.decls[idx] = Std.Sat.AIG.Decl.atom x ∧ a = r x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  (Std.DHashMap.filterMap f m).getKey? k =
    (m.getKey? k).pfilter fun x_2 h' => (f x_2 (Std.DHashMap.Const.get m x_2 ⋯)).isSome
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.prime_p : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Prime ↑p
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.isLocalHom_expand : ∀ (R : Type u_1) (σ : Type u_2) [inst : CommRing R] {p : ℕ}, p ≠ 0 → IsLocalHom (MvPolynomial.expand p)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Option.isSome.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : (val : α) → motive (some val))
  (h_2 : Unit → motive none),
  (match some val with
    | some val => h_1 val
    | none => h_2 ()) =
    h_1 val
-- Mathlib.Analysis.InnerProductSpace.Adjoint
InnerProductSpace.rankOne_comp : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {E : Type u_5} {G : Type u_6} [inst_4 : SeminormedAddCommGroup E]
  [inst_5 : NormedSpace 𝕜 E] [inst_6 : NormedAddCommGroup G] [inst_7 : InnerProductSpace 𝕜 G] [inst_8 : CompleteSpace G]
  (x : E) (y : F) (f : G →L[𝕜] F),
  ((InnerProductSpace.rankOne 𝕜) x) y ∘SL f = ((InnerProductSpace.rankOne 𝕜) x) ((ContinuousLinearMap.adjoint f) y)
-- Mathlib.GroupTheory.Index
/-- Relative version of `Subgroup.index_eq_two_iff_exists_notMem_and`.  -/
Subgroup.relIndex_eq_two_iff_exists_notMem_and : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H
-- Mathlib.RingTheory.Unramified.Basic
/-- Unramified is stable under base change.  -/
Algebra.Unramified.baseChange : ∀ (R : Type u_1) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.Unramified R A], Algebra.Unramified B (TensorProduct R B A)
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.instIsMarkovKernelCondExpKernel : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.condExpKernel μ m)
-- Batteries.Data.List.Lemmas
List.getElem_swap : ∀ {α : Type u_1} {xs : List α} {i j k : ℕ} (hk : k < (xs.swap i j).length),
  (xs.swap i j)[k] = if h₁ : k = i ∧ j < xs.length then xs[j] else if h₂ : k = j ∧ i < xs.length then xs[i] else xs[k]
-- Mathlib.Analysis.Normed.Module.TransferInstance
Equiv.normedAddCommGroup.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] (e : α ≃ β),
  e.normedAddCommGroup =
    { toNorm := (NormedAddCommGroup.induced α β e.addEquiv ⋯).toNorm,
      toAddCommGroup := (NormedAddCommGroup.induced α β e.addEquiv ⋯).toAddCommGroup,
      toPseudoMetricSpace := e.pseudometricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff m₂ ⋯).getKey! k = m₁.getKey! k
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.isHomogeneous_of_isEmpty : ∀ (σ : Type u_1) (R : Type u_3) [inst : CommSemiring R] [IsEmpty σ] (f : MvPolynomial σ R), f.IsHomogeneous 0
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instFibrationUnopOfCofibrationOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : Cᵒᵖ} (f : X ⟶ Y) [HomotopicalAlgebra.Cofibration f], HomotopicalAlgebra.Fibration f.unop
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
ProbabilityTheory.HasIndepIncrements.nat : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : Preorder T] [inst_1 : MeasurableSpace E] [inst_2 : Sub E],
  ProbabilityTheory.HasIndepIncrements X P →
    ∀ {t : ℕ → T}, Monotone t → ProbabilityTheory.iIndepFun (fun i ω => X (t (i + 1)) ω - X (t i) ω) P
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_add_neg_iff_add_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b c : α}, c ≤ a + -b ↔ c + b ≤ a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.typeParameter : Lean.Lsp.CompletionItemKind
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr'Aux_foldr'Aux : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N),
  (∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx) →
    ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
      ((CliffordAlgebra.foldr'Aux Q f) v) (((CliffordAlgebra.foldr'Aux Q f) v) x_fx) = Q v • x_fx
-- Mathlib.Probability.Kernel.Category.Stoch
instDeterministicStochComul : ∀ {X : Stoch}, CategoryTheory.Deterministic CategoryTheory.ComonObj.comul
-- Lean.Meta.Tactic.Cases
Lean.Meta.CasesSubgoal.mk.sizeOf_spec : ∀ (toInductionSubgoal : Lean.Meta.InductionSubgoal) (ctorName : Option Lean.Name),
  sizeOf { toInductionSubgoal := toInductionSubgoal, ctorName := ctorName } =
    1 + sizeOf toInductionSubgoal + sizeOf ctorName
-- Mathlib.Algebra.Category.ModuleCat.Kernels
ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (ModuleCat.cokernelIsoRangeQuotient f).hom =
    ModuleCat.ofHom (ModuleCat.Hom.hom f).range.mkQ
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.weakPullback.lift_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C} (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakPullback.lift h k w)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakPullback.snd f g) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Algebra.Order.ToIntervalMod
_private.Mathlib.Algebra.Order.ToIntervalMod.0.toIxxMod_total : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b c : α), toIcoMod hp a b ≤ toIocMod hp a c ∨ toIcoMod hp c b ≤ toIocMod hp c a
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInterClosure.below.univ : ∀ {α : Type u_1} {S : Set (Set α)} {motive : (a : Set α) → FiniteInter.finiteInterClosure S a → Prop},
  FiniteInter.finiteInterClosure.below ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- A subsemiring is an `ℕ`-subalgebra.  -/
subalgebraOfSubsemiring : {R : Type u_1} → [inst : Semiring R] → Subsemiring R → Subalgebra ℕ R
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Combine two `PartialEquiv`s using `Set.piecewise`. The source of the new `PartialEquiv` is
`s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s`, and similarly for target.  The function
sends `e.source ∩ s` to `e.target ∩ t` using `e` and `e'.source \ s` to `e'.target \ t` using `e'`,
and similarly for the inverse function. The definition assumes `e.isImage s t` and
`e'.isImage s t`.  -/
PartialEquiv.piecewise : {α : Type u_1} →
  {β : Type u_2} →
    (e e' : PartialEquiv α β) →
      (s : Set α) →
        (t : Set β) →
          [(x : α) → Decidable (x ∈ s)] →
            [(y : β) → Decidable (y ∈ t)] → e.IsImage s t → e'.IsImage s t → PartialEquiv α β
-- Mathlib.Topology.DiscreteSubset
/-- **Alias** of the forward direction of `isDiscrete_iff_nhdsWithin`. -/
IsDiscrete.nhdsWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s → ∀ x ∈ s, nhdsWithin x s = pure x
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_uInt32ToNat : ∀ (n : UInt32), UInt64.ofNatLT n.toNat ⋯ = n.toUInt64
-- Init.Data.UInt.Lemmas
UInt64.sub_zero : ∀ (a : UInt64), a - 0 = a
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonneg_mul : ∀ {d : ℕ} {a b : ℤ√↑d}, a.Nonneg → b.Nonneg → (a * b).Nonneg
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- The free abelian group on a type with one term is isomorphic to `ℤ`.  -/
FreeAbelianGroup.uniqueEquiv : (T : Type u_2) → [Unique T] → FreeAbelianGroup T ≃+ ℤ
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_one_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [NeZero μ] [inst_3 : One β] {x : α}, ↑1 x = 1
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsNonloopAt.of_compatible : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β},
  G.Compatible H → e ∈ H.edgeSet → G.IsNonloopAt e x → H.IsNonloopAt e x
-- Mathlib.Geometry.Euclidean.Simplex
/-- The distance from a vertex to the `centroid` equals `n` times the distance from the `centroid`
to the corresponding `faceOppositeCentroid`.  -/
Affine.Simplex.dist_point_centroid : ∀ {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) (i : Fin (n + 1)),
  dist (s.points i) s.centroid = ↑n * dist s.centroid (s.faceOppositeCentroid i)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm_one : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GSemiring 𝒜] [inst_9 : DirectSum.GSemiring ℬ], (TensorProduct.gradedComm R 𝒜 ℬ) 1 = 1
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_eq_of_eRk_insert_le_forall : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, X ⊆ Y → (∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X) → M.eRk X = M.eRk Y
-- Aesop.RuleTac.GoalDiff
Aesop.GoalDiff.mk.injEq : ∀ (oldGoal newGoal : Lean.MVarId) (addedFVars removedFVars : Std.HashSet Lean.FVarId) (targetChanged : Bool)
  (oldGoal_1 newGoal_1 : Lean.MVarId) (addedFVars_1 removedFVars_1 : Std.HashSet Lean.FVarId) (targetChanged_1 : Bool),
  ({ oldGoal := oldGoal, newGoal := newGoal, addedFVars := addedFVars, removedFVars := removedFVars,
        targetChanged := targetChanged } =
      { oldGoal := oldGoal_1, newGoal := newGoal_1, addedFVars := addedFVars_1, removedFVars := removedFVars_1,
        targetChanged := targetChanged_1 }) =
    (oldGoal = oldGoal_1 ∧
      newGoal = newGoal_1 ∧ addedFVars = addedFVars_1 ∧ removedFVars = removedFVars_1 ∧ targetChanged = targetChanged_1)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimit_of_hasLimit_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [CategoryTheory.Limits.HasLimit F.unop], CategoryTheory.Limits.HasColimit F
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- A (not necessarily bounded) operator on an inner product space is symmetric, if for all
`x`, `y`, we have `⟪T x, y⟫ = ⟪x, T y⟫`.  -/
LinearMap.IsSymmetric : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → (E →ₗ[𝕜] E) → Prop
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.imp.inj : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {f₁ f₂ f₁_1 f₂_1 : L.BoundedFormula α n},
  f₁.imp f₂ = f₁_1.imp f₂_1 → f₁ = f₁_1 ∧ f₂ = f₂_1
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- The functor `Cocone.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F)` is a left adjoint.  -/
CategoryTheory.Adjunction.functorialityAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  (K : CategoryTheory.Functor J C) →
                    CategoryTheory.Limits.Cocone.functoriality K F ⊣ adj.functorialityRightAdjoint K
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.seq1.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.of_norm_eventuallyEq_norm : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  ((fun x => ‖f x‖) =ᶠ[l] fun x => ‖g x‖) → f =Θ[l] g
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.mulEquivCongr_mapSubgroup_fixingSubgroup : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : IsDomain B] [inst_5 : Algebra A B] [inst_6 : FaithfulSMul A B]
  [inst_7 : MulSemiringAction G B] [inst_8 : MulSemiringAction G' B] [inst_9 : IsGaloisGroup G A B]
  [inst_10 : IsGaloisGroup G' A B] [inst_11 : Finite G] [inst_12 : Finite G'] (S : Set B),
  Subgroup.map (↑(IsGaloisGroup.mulEquivCongr G G' A B)) (fixingSubgroup G S) = fixingSubgroup G' S
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rco : ∀ {m n i : ℕ}, (m...n).toArray[i]? = if i < n - m then some (m + i) else none
-- Aesop.RuleTac.Basic
Aesop.RuleApplication.check : Aesop.RuleApplication → Aesop.RuleTacInput → Aesop.BaseM (Option Lean.MessageData)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] {k k' : α} {f : Option β → Option β} {hc : k' ∈ t.alter k f},
  (t.alter k f).getKey k' hc = if heq : cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
/-- Given arithmetic functions `f(q⁻ˢ)` with `q → ∞`, the partial products `∏ i ∈ s, f i` converge
to the Euler product pointwise.  -/
ArithmeticFunction.tendsTo_eulerProduct_ofPowerSeries : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] (q : ι → ℕ) [hq : Northcott q] (f : ι → PowerSeries R),
  (∀ (i : ι), PowerSeries.constantCoeff (f i) = 1) →
    ∀ (n : ℕ),
      ∀ᶠ (s : Finset ι) in Filter.atTop,
        (∏ i ∈ s, (ArithmeticFunction.ofPowerSeries (q i)) (f i)) n =
          (ArithmeticFunction.eulerProduct fun i => (ArithmeticFunction.ofPowerSeries (q i)) (f i)) n
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Non commutative rings.
 -/
Lean.Meta.Grind.Arith.CommRing.State.ncRings : Lean.Meta.Grind.Arith.CommRing.State → Array Lean.Meta.Grind.Arith.CommRing.Ring
-- Lean.Parser.Term
Lean.Parser.Term.show : Lean.Parser.Parser
-- Mathlib.Analysis.RCLike.Basic
RCLike.realRingEquiv_apply : ∀ {K : Type u_1} [inst : RCLike K] (h : RCLike.I = 0) (a : K), (RCLike.realRingEquiv h) a = RCLike.re a
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
IsCovariantDerivativeOn.torsion_antisymm : ∀ {𝕜 : 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] {x : M} [inst_6 : IsManifold I 2 M]
  [inst_7 : CompleteSpace E] {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x}
  [inst_8 : CompleteSpace 𝕜] [inst_9 : FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov)
  (X₀ Y₀ : TangentSpace I x), ((hcov.torsion x) X₀) Y₀ = -((hcov.torsion x) Y₀) X₀
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the `n`-th smallest key.  -/
Std.ExtDTreeMap.keyAtIdx : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → (n : ℕ) → n < t.size → α
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.isAddUnit_comp : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) (j : N →+ P) (y : ↥S), IsAddUnit ((j.comp f.toAddMonoidHom) ↑y)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLTD_eq_getD_getEntryLT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α} {fallback : (a : α) × β a},
  Std.DTreeMap.Internal.Impl.getEntryLTD k t fallback = (Std.DTreeMap.Internal.Impl.getEntryLT? k t).getD fallback
-- Mathlib.Analysis.Analytic.OfScalars
/-- The submodule generated by scalar series on `FormalMultilinearSeries 𝕜 E E`.  -/
FormalMultilinearSeries.ofScalarsSubmodule : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : Field 𝕜] →
      [inst_1 : Ring E] →
        [inst_2 : Algebra 𝕜 E] →
          [inst_3 : TopologicalSpace E] → [inst_4 : IsTopologicalRing E] → Submodule 𝕜 (FormalMultilinearSeries 𝕜 E E)
-- Mathlib.RepresentationTheory.Invariants
Representation.invariants_eq_inter : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V), ρ.invariants.carrier = ⋂ g, Function.fixedPoints ⇑(ρ g)
-- Mathlib.Data.List.Cycle
Cycle.next_mem : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x ∈ s), s.next hs x hx ∈ s
-- Mathlib.Algebra.Polynomial.RuleOfSigns
Polynomial.signVariations.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] (P : Polynomial R),
  P.signVariations =
    (List.destutter (fun x1 x2 => x1 ≠ x2)
          (List.filter (fun x => decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1
-- Init.Data.AC
Lean.Data.AC.Context.comm : {α : Sort u} → (self : Lean.Data.AC.Context α) → Option (PLift (Std.Commutative self.op))
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (f : MvPowerSeries σ R), f ≠ 0 ↔ ∃ d, (MvPowerSeries.coeff d) f ≠ 0
-- Lean.Meta.Basic
Lean.Meta.getLocalInstances : Lean.MetaM Lean.LocalInstances
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instSemilatticeSup : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [SemilatticeSup β] → SemilatticeSup (MeasureTheory.SimpleFunc α β)
-- Mathlib.Topology.AlexandrovDiscrete
AlexandrovDiscrete.mk : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  (∀ (S : Set (Set α)), (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)) → AlexandrovDiscrete α
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartRing.mk : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  [inst_3 : LieRingModule L A],
  (∀ (a b : A) (x : L), ⁅a • x, b⁆ = a * ⁅x, b⁆) →
    (∀ (x : L) (a b : A), ⁅x, a * b⁆ = a • ⁅x, b⁆ + ⁅x, a⁆ * b) →
      (∀ (x y : L) (a : A), ⁅x, a • y⁆ = a • ⁅x, y⁆ + ⁅x, a⁆ • y) → LieRinehartRing A L
-- Mathlib.Algebra.Field.Rat
NNRat.instSemifield : Semifield ℚ≥0
-- Mathlib.Order.Disjoint
/-- **Alias** of the forward direction of `codisjoint_self`. -/
Codisjoint.eq_top_of_self : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, Codisjoint a a → a = ⊤
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] →
        (toEquiv : α ≃ β) →
          autoParam (Measurable ⇑toEquiv) MeasurableEquiv.measurable_toFun._autoParam →
            autoParam (Measurable ⇑toEquiv.symm) MeasurableEquiv.measurable_invFun._autoParam → α ≃ᵐ β
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Expressions for atomic structural 2-morphisms.  -/
Mathlib.Tactic.BicategoryLike.StructuralAtom : Type
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.leftRel_apply : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, (QuotientAddGroup.leftRel s) x y ↔ -x + y ∈ s
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.lookahead.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₂ : ∀ (pq : ℕ × ℕ), CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat.i₂ pq = WithBotTop.coe (-↑pq.2 + 1)
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.lift_sepDegree_bot' : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  Cardinal.lift.{v, w} (Field.sepDegree F ↥⊥) = Cardinal.lift.{w, v} (Field.sepDegree F E)
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.uniformEquicontinuous_iff_left : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {p : κ → Prop}
  {s : κ → Set (β × β)} {F : ι → β → α},
  (uniformity β).HasBasis p s →
    (UniformEquicontinuous F ↔ ∀ U ∈ uniformity α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U)
-- Init.Data.Ord.String
Char.instLawfulEqOrd : Std.LawfulEqOrd Char
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.sup_assoc : ∀ {α : Type u_1} [inst : BooleanRing α] (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.card_stabilizer : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K} [IsGalois k K],
  Nat.card ↥(MulAction.stabilizer Gal(K/k) w) = if NumberField.InfinitePlace.IsUnramified k w then 1 else 2