mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.NNRat.BigOperators
NNRat.cast_listSum : ∀ {K : Type u_2} [inst : DivisionSemiring K] [CharZero K] (l : List ℚ≥0), ↑l.sum = (List.map NNRat.cast l).sum
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.invFunIdAssoc_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (F : CategoryTheory.Functor D E) (X : D),
  (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)
-- Init.Data.Int.DivMod.Basic
_private.Init.Data.Int.DivMod.Basic.0.Int.fdiv.match_1.eq_1 : ∀ (motive : ℤ → ℤ → Sort u_1) (x : ℤ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match 0, x with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc a, 0 => h_4 a
    | Int.negSucc m, Int.ofNat n.succ => h_5 m n
    | Int.negSucc m, Int.negSucc n => h_6 m n) =
    h_1 x
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.ne_bot_iff_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C), ¬P = ⊥ ↔ ∃ X, P X
-- Mathlib.Algebra.Ring.Action.Submonoid
FixedPoints.mem_addSubmonoid : ∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : AddMonoid α] [inst_2 : DistribMulAction M α] (a : α),
  a ∈ FixedPoints.addSubmonoid M α ↔ ∀ (m : M), m • a = a
-- Lean.Server.InfoUtils
Lean.Elab.instBEqHoverableInfoPrio.beq : Lean.Elab.HoverableInfoPrio → Lean.Elab.HoverableInfoPrio → Bool
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.IsReduced.red_iff_eq : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.IsReduced L₁ → (FreeGroup.Red L₁ L₂ ↔ L₂ = L₁)
-- Mathlib.Tactic.Linter.UnusedTactic
/-- Adds a new syntax kind whose children will be ignored by the `unusedTactic` linter.
This should be called from an `initialize` block.
 -/
_private.Mathlib.Tactic.Linter.UnusedTactic.0.Mathlib.Linter.UnusedTactic.addIgnoreTacticKind : Lean.SyntaxNodeKind → IO Unit
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.toDeleteEdges_copy : ∀ {V : Type u} (G : SimpleGraph V) {v u u' v' : V} (s : Set (Sym2 V)) (p : G.Walk u v) (hu : u = u') (hv : v = v')
  (h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s),
  SimpleGraph.Walk.toDeleteEdges s (p.copy hu hv) h = (SimpleGraph.Walk.toDeleteEdges s p ⋯).copy hu hv
-- Lean.Data.OpenDecl
Lean.OpenDecl.explicit.sizeOf_spec : ∀ (id declName : Lean.Name), sizeOf (Lean.OpenDecl.explicit id declName) = 1 + sizeOf id + sizeOf declName
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_one_left' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a : α), Associated (gcd 1 a) 1
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mapIso_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C} (e : A ≅ B),
  (CategoryTheory.MonoOver.mapIso e).counitIso =
    (CategoryTheory.MonoOver.mapComp e.inv e.hom).symm ≪≫ CategoryTheory.eqToIso ⋯ ≪≫ CategoryTheory.MonoOver.mapId B
-- Mathlib.Data.List.Chain
List.IsChain.iterate_eq_of_apply_eq : ∀ {α : Type u_3} {f : α → α} {l : List α},
  List.IsChain (fun x y => f x = y) l → ∀ (i : ℕ) (hi : i < l.length), f^[i] l[0] = l[i]
-- Mathlib.Data.List.Cycle
/-- `Cycle α` is the quotient of `List α` by cyclic permutation.
Duplicates are allowed.
 -/
Cycle : Type u_1 → Type u_1
-- Init.Data.String.Basic
String.Slice.Pos.str_ne_endPos : ∀ {s : String.Slice} (p : s.Pos), p ≠ s.endPos → p.str ≠ s.str.endPos
-- Lean.Parser.Basic
Lean.Parser.OrElseOnAntiquotBehavior.merge : Lean.Parser.OrElseOnAntiquotBehavior
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerTMul_smul : ∀ (R : Type u_1) {S : Type u_2} {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11}
  {p : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β] [inst_5 : Monoid S] [inst_6 : DistribMulAction S α] [inst_7 : DistribMulAction S β]
  [inst_8 : SMul S R] [inst_9 : SMulCommClass R S α] [IsScalarTower S R α] [IsScalarTower S R β] (r : S)
  (A : Matrix l m α) (B : Matrix n p β),
  Matrix.kroneckerMap (TensorProduct.tmul R) A (r • B) = r • Matrix.kroneckerMap (TensorProduct.tmul R) A B
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
/-- Equivalence of groupoids between fundamental groupoid of punit and punit  -/
FundamentalGroupoid.punitEquivDiscretePUnit : FundamentalGroupoid PUnit.{u + 1} ≌ CategoryTheory.Discrete PUnit.{v + 1}
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instQuasiIsoMapOppositeSymmUnopFunctorOp : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L)
  [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i] [QuasiIso φ],
  QuasiIso ((HomologicalComplex.unopFunctor V c).map φ.op)
-- Std.Async.System
/-- Time spent servicing hardware interrupts.
 -/
Std.Async.System.CPUTimes.interruptTime : Std.Async.System.CPUTimes → Std.Time.Millisecond.Offset
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
instLeftCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsLeftCancelMulZero : {M₀ : Type u_2} →
  [inst : MonoidWithZero M₀] → [Nontrivial M₀] → [IsLeftCancelMulZero M₀] → LeftCancelMonoid ↥(nonZeroDivisors M₀)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.piPremeasure_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] {m : (i : ι) → MeasureTheory.OuterMeasure (α i)}
  {s : (i : ι) → Set (α i)}, (Set.univ.pi s).Nonempty → MeasureTheory.piPremeasure m (Set.univ.pi s) = ∏ i, (m i) (s i)
-- Lean.Linter.UnusedVariables
/-- A mapping from alias to original FVarId. We don't guarantee that the value is not itself
an alias, but we use `followAliases` when adding new elements to try to avoid long chains.  -/
Lean.Linter.UnusedVariables.References.fvarAliases : Lean.Linter.UnusedVariables.References → Std.HashMap Lean.FVarId Lean.FVarId
-- Mathlib.MeasureTheory.SetAlgebra
/-- An algebra of sets is closed by finite unions.  -/
MeasureTheory.IsSetAlgebra.biUnion_mem : ∀ {α : Type u_1} {𝒜 : Set (Set α)} {ι : Type u_2},
  MeasureTheory.IsSetAlgebra 𝒜 → ∀ {s : ι → Set α} (S : Finset ι), (∀ i ∈ S, s i ∈ 𝒜) → ⋃ i ∈ S, s i ∈ 𝒜
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_neg_pi_div_two : 2 • ↑(-Real.pi / 2) = ↑Real.pi
-- Mathlib.Algebra.Ring.Center
Set.natCast_mem_center : ∀ (M : Type u_1) [inst : NonAssocSemiring M] (n : ℕ), ↑n ∈ Set.center M
-- Init.Prelude
/-- Make name `s₁`  -/
Lean.Name.mkStr1 : String → Lean.Name
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.balancedAtRoot_two_one : Std.DTreeMap.Internal.Impl.BalancedAtRoot 2 1
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Adjunction.unop_unit : ∀ {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ᵒᵖ} (h : G ⊣ F),
  h.unop.unit = CategoryTheory.NatTrans.unop h.counit
-- Mathlib.Tactic.Ring.Basic
/-- The data used by the `ring` tactic to normalize the constant coefficients.  -/
Mathlib.Tactic.Ring.ringCompute : {u : Lean.Level} →
  {α : Q(Type u)} →
    {sα : Q(CommSemiring «$α»)} →
      Mathlib.Tactic.Ring.Common.Cache sα → Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.RatCoeff sα
-- Mathlib.NumberTheory.SelbergSieve
/-- The weight of all the elements that are not a multiple of any of our finite set of primes.  -/
BoundingSieve.siftedSum : {s : BoundingSieve} → ℝ
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.foldM_map : ∀ {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 : β → γ} {g : δ → γ → n δ} {init : δ}
  {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄ Std.Iter.foldM (fun d b => g d (f b)) init it ⦃Q⦄ → ⦃P⦄ Std.Iter.foldM g init (Std.Iter.map f it) ⦃Q⦄
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.instPartialOrderCoconePt : {J : Type u} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] →
      {F : CategoryTheory.Functor J PartOrdEmb} →
        {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} →
          (hc : CategoryTheory.Limits.IsColimit c) → PartialOrder (PartOrdEmb.Limits.CoconePt hc)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.smul_inv : ∀ {k : Type u_2} [inst : Field k] (r : k) (φ : PowerSeries k), (r • φ)⁻¹ = r⁻¹ • φ⁻¹
-- Mathlib.Data.List.SplitLengths
List.length_splitLengths_getElem_le : ∀ {α : Type u_1} (l : List α) (sz : List ℕ) {i : ℕ} {hi : i < (sz.splitLengths l).length},
  (sz.splitLengths l)[i].length ≤ sz[i]
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.mkEncodableCmds : Lean.InductiveVal → Array Lean.Name → Lean.Elab.TermElabM (Array Lean.Syntax)
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.compRight_compLeft : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) (l r : M →ₗ[R] M), (B.compRight r).compLeft l = B.comp l r
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.height_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R] (i : ι), b.height i ≠ 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map.eq_1 : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {basis_hd' : ℝ → ℝ}
  {basis_tl' : Tactic.ComputeAsymptotics.Basis} (f : ℝ → ℝ)
  (g :
    Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl → Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl')
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map f g ms =
    Stream'.Seq.map
      (fun x =>
        match x with
        | (exp, coef) => (f exp, g coef))
      ms
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.instBraidedCategoryLocalizedMonoidal : {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) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      [CategoryTheory.BraidedCategory C] →
                        CategoryTheory.BraidedCategory (CategoryTheory.LocalizedMonoidal L W ε)
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.topSort.visit : Array Lean.Expr → Lean.Expr → Lean.Elab.Term.ToDepElimPattern.TopSortM Unit
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Formula for `completedHurwitzZetaEven` as a Dirichlet series in the convergence range.  -/
HurwitzZeta.hasSum_int_completedHurwitzZetaEven : ∀ (a : ℝ) {s : ℂ},
  1 < s.re → HasSum (fun n => s.Gammaℝ / ↑|↑n + a| ^ s / 2) (HurwitzZeta.completedHurwitzZetaEven (↑a) s)
-- Lean.Elab.MutualInductive
/-- Decides whether the inductive type should be `Prop`-valued when the universe is not given.

Heuristic:
- We want `Prop` when each inductive type is obviously a syntactic subsingleton.
  That's to say, when each inductive type has at most one constructor, and each field is a `Prop`.
  Such types carry no data anyway.
- Exception: if no inductive type has any constructors, these are likely stubbed-out declarations,
  so we prefer `Type` instead.
- Exception: if each constructor has no parameters, then these are likely partially-written enumerations,
  so we prefer `Type` instead.

When ppecialized to structures, the heuristic is that we prefer a `Prop` instead of a `Type` structure
when it could be a syntactic subsingleton.
Exception: no-field structures are `Type` since they are likely stubbed-out declarations.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.isPropCandidate : ℕ → List Lean.InductiveType → Array Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.Interval.Finset.Basic
Finset.card_Iio_eq_card_Iic_sub_one : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderBot α] (a : α),
  (Finset.Iio a).card = (Finset.Iic a).card - 1
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_eq_stoppedValue_apply : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] (i : ι) (ω : Ω),
  MeasureTheory.stoppedProcess u τ i ω = MeasureTheory.stoppedValue u (fun ω => min (↑i) (τ ω)) ω
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMap.mk.sizeOf_spec : ∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂]
  [inst_6 : SizeOf A₁] [inst_7 : SizeOf A₂] (toLinearMap : A₁ →ₗ[ℂ] A₂)
  (map_cstarMatrix_nonneg' : ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap),
  sizeOf { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' } = 1 + sizeOf toLinearMap
-- Init.Data.Iterators.Basic
Std.Iterator.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : outParam (Type w)} →
      (IsPlausibleStep : Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop) →
        ((it : Std.IterM m β) → m (Std.Shrink (Std.PlausibleIterStep (IsPlausibleStep it)))) → Std.Iterator α m β
-- Mathlib.Analysis.Calculus.ContDiff.Comp
contDiff_prod_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} (f : E → F × G),
  ContDiff 𝕜 n f ↔ ContDiff 𝕜 n (Prod.fst ∘ f) ∧ ContDiff 𝕜 n (Prod.snd ∘ f)
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.PlausibleStep.sndDone : ∀ {m : Type w → Type w'} {β α₁ α₂ : Type w} [inst : Std.Iterator α₁ m β] [inst_1 : Std.Iterator α₂ m β]
  {it₂ : Std.IterM m β},
  it₂.IsPlausibleStep Std.IterStep.done →
    Std.Iterators.Types.Append.PlausibleStep (Std.IterM.Intermediate.appendSnd α₁ it₂) Std.IterStep.done
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂)[k] = t₂[k]
-- Mathlib.Topology.Algebra.Monoid.Defs
Continuous.const_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M}, Continuous f → ∀ (b : M), Continuous fun x => b * f x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.OplaxTrans F G) {a b c : B} (f : a ⟶ b)
  (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f) (G.map g))
              (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_def : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [hq : q.IsPrime] [inst_3 : Algebra (Localization.AtPrime (Ideal.under R q)) (Localization.AtPrime q)]
  [inst_4 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R q) q],
  q.inertiaDeg R = Module.finrank (Ideal.under R q).ResidueField q.ResidueField
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- The bijection allows us to show that `prodComparison L A B` is an isomorphism, where the inverse
is the forward map of the identity morphism.
 -/
CategoryTheory.prodComparison_iso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.Reflective i] [inst_4 : CategoryTheory.MonoidalClosed C]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory D] [CategoryTheory.ExponentialIdeal i]
  [CategoryTheory.BraidedCategory C] (A B : C),
  CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison (CategoryTheory.reflector i) A B)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Zipper α β → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : Std.DTreeMap.Internal.Zipper α β)
  (h_1 : (it : Std.DTreeMap.Internal.Zipper α β) → motive Std.DTreeMap.Internal.Impl.leaf it)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (it : Std.DTreeMap.Internal.Zipper α β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) it)
  (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (it : Std.DTreeMap.Internal.Zipper α β),
  x = Std.DTreeMap.Internal.Impl.inner size k v l r →
    x_1 = it →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.leaf, it => h_1 it
        | Std.DTreeMap.Internal.Impl.inner size k v l r, it => h_2 size k v l r it) ≍
        h_2 size k v l r it
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The induced map from the quotient by the kernel to the codomain.

This is an isomorphism if `f` has a right inverse (`quotientKerEquivOfRightInverse`) /
is surjective (`quotientKerEquivOfSurjective`).
 -/
RingHom.kerLift : {R : Type u} → {S : Type v} → [inst : Ring R] → [inst_1 : Semiring S] → (f : R →+* S) → R ⧸ RingHom.ker f →+* S
-- Lean.Server.CodeActions.Provider
/-- A code action which calls all `@[command_code_action]` code actions on each command.
 -/
Lean.CodeAction.cmdCodeActionProvider : Lean.Server.CodeActionProvider
-- Lean.MetavarContext
/-- Assignment table for universe level metavariables. -/
Lean.MetavarContext.lAssignment : Lean.MetavarContext → Lean.PersistentHashMap Lean.LMVarId Lean.Level
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_mul : ∀ {d : ℤ} (z w : ℤ√d), (z * w).im = z.re * w.im + z.im * w.re
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
le_iff_norm_sqrt_mul_sqrt_inv : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {a : A} {b : Aˣ},
  0 ≤ a → 0 ≤ ↑b → (a ≤ ↑b ↔ ‖CFC.sqrt a * CFC.sqrt ↑b⁻¹‖ ≤ 1)
-- Mathlib.Order.Interval.Set.IsoIoo
/-- In a linear ordered field, the whole field is order isomorphic to the open interval `(-1, 1)`.
We consider the actual implementation to be a "black box", so it is irreducible.
 -/
orderIsoIooNegOneOne : (k : Type u_1) → [inst : Field k] → [inst_1 : LinearOrder k] → [IsStrictOrderedRing k] → k ≃o ↑(Set.Ioo (-1) 1)
-- Batteries.Data.List.Lemmas
List.append_eq_of_isPrefixOf?_eq_some : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs ys zs : List α}, xs.isPrefixOf? ys = some zs → xs ++ zs = ys
-- Mathlib.Data.PEquiv
PEquiv.mem_single : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (a : α) (b : β), b ∈ (PEquiv.single a b) a
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeft_map_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y),
  ((CategoryTheory.Comma.mapLeft R l).map f).right = f.right
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_iff_map_le : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom H ≤ H
-- Mathlib.Algebra.MvPolynomial.Polynomial
MvPolynomial.eval_polynomial_eval_finSuccEquiv : ∀ {R : Type u_1} {n : ℕ} {x : Fin n → R} [inst : CommSemiring R] (f : MvPolynomial (Fin (n + 1)) R)
  (q : MvPolynomial (Fin n) R),
  (MvPolynomial.eval x) (Polynomial.eval q ((MvPolynomial.finSuccEquiv R n) f)) =
    (MvPolynomial.eval fun i => Fin.cases ((MvPolynomial.eval x) q) x i) f
-- Init.Data.Nat.Lemmas
Nat.exists_eq_add_of_le : ∀ {m n : ℕ}, m ≤ n → ∃ k, n = m + k
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.nonReservedSymbolNoAntiquot.formatter : String → Lean.PrettyPrinter.Formatter
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.Context.except : Lean.MetavarContext.LevelMVarToParam.Context → Lean.LMVarId → Bool
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.toGermAddMonoidHom.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddMonoid γ] [inst_3 : ContinuousAdd γ],
  MeasureTheory.AEEqFun.toGermAddMonoidHom = { toFun := MeasureTheory.AEEqFun.toGerm, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.LinearAlgebra.Dimension.DivisionRing
/-- This is mostly an auxiliary lemma for `Submodule.rank_sup_add_rank_inf_eq`.  -/
rank_add_rank_split : ∀ {K : Type u} {V V₁ V₂ V₃ : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₁] [inst_4 : Module K V₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module K V₂]
  [inst_7 : AddCommGroup V₃] [inst_8 : Module K V₃] (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd : V₁ →ₗ[K] V₂)
  (ce : V₁ →ₗ[K] V₃),
  ⊤ ≤ db.range ⊔ eb.range →
    cd.ker = ⊥ →
      db ∘ₗ cd = eb ∘ₗ ce →
        (∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e) →
          Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.isPos_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R] {i : ι}, b.IsPos i ↔ 0 < b.height i
-- Mathlib.Data.Finset.Powerset
/-- For predicate `p` decidable on subsets, it is decidable whether `p` holds for every subset.  -/
Finset.decidableForallOfDecidableSubsets : {α : Type u_1} →
  {s : Finset α} →
    {p : (t : Finset α) → t ⊆ s → Prop} →
      [(t : Finset α) → (h : t ⊆ s) → Decidable (p t h)] → Decidable (∀ (t : Finset α) (h : t ⊆ s), p t h)