mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Interleave
/-- Interleave two lists `l₁` and `l₂`, starting with an element of `l₁`.

This operation fully interleave the two lists when the length of `l₁` is either the length of `l₂`
or one more. If one of the lists runs out early, the remainder of the other list is kept without
further interleaving, so that `l₁.interleave l₂` is always a permutation of `l₁ ++ l₂`.
See `interleave_perm_append`.

```
#eval interleave [0, 2, 4] [1] -- [0, 1, 2, 4] -- The second list is too short
#eval interleave [0, 2, 4] [1, 3] -- [0, 1, 2, 3, 4]
#eval interleave [0, 2] [1, 3] -- [0, 1, 2, 3]
#eval interleave [0] [1, 3] -- [0, 1, 3] -- The first list is too short
```
 -/
List.interleave : {α : Type u_1} → List α → List α → List α
-- Init.Data.List.Erase
List.Nodup.mem_erase_iff : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {b : α} [LawfulBEq α] {a : α}, l.Nodup → (a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l)
-- Mathlib.Combinatorics.Configuration
Configuration.HasPoints.mkPoint_ax : ∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.HasPoints P L] {l₁ l₂ : L} (h : l₁ ≠ l₂),
  Configuration.HasPoints.mkPoint h ∈ l₁ ∧ Configuration.HasPoints.mkPoint h ∈ l₂
-- Mathlib.FieldTheory.Minpoly.Field
/-- See also `minpoly.ker_eval` which relaxes the assumptions on `A` in exchange for
stronger assumptions on `B`.  -/
minpoly.ker_aeval_eq_span_minpoly : ∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B),
  RingHom.ker (Polynomial.aeval x) = Polynomial A ∙ minpoly A x
-- Init.Prelude
_private.Init.Prelude.0.Lean.Macro.State.expandedMacroDecls : Lean.Macro.State → List Lean.Name
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.X_inv : ∀ {k : Type u_2} [inst : Field k], PowerSeries.X⁻¹ = 0
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
GaloisConnection.u_csInf_of_directedOn : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderInf α]
  [inst_1 : ConditionallyCompletePartialOrderInf β] {l : α → β} {u : β → α},
  GaloisConnection u l →
    ∀ {s : Set α}, DirectedOn (fun x1 x2 => x2 ≤ x1) s → s.Nonempty → BddBelow s → l (sInf s) = ⨅ x, l ↑x
-- Mathlib.Data.Finset.Dedup
List.toFinset_surj_on : ∀ {α : Type u_1} [inst : DecidableEq α], Set.SurjOn List.toFinset {l | l.Nodup} Set.univ
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.eq_of_mem_uIoc_of_mem_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ∈ Set.uIoc b c → b ∈ Set.uIoc a c → a = b
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sSup_zero : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : Zero M], sSup 0 = 0
-- Mathlib.Algebra.Lie.Basic
LieEquiv.coe_toLinearEquiv : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂), ⇑e.toLinearEquiv = ⇑e
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyRel.exists_good_cylinder : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {f g : X ⟶ Y}, HomotopicalAlgebra.LeftHomotopyRel f g → ∃ P, P.IsGood ∧ Nonempty (P.LeftHomotopy f g)
-- Init.Data.Order.LemmasExtra
Std.max_eq_if_isGE_compare : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] {x : Max α} [Std.LawfulOrderOrd α] [Std.LawfulOrderLeftLeaningMax α]
  {a b : α}, a ⊔ b = if (compare a b).isGE = true then a else b
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Convenience shortcut for `Rep.hom_bijective.surjective`.  -/
Rep.hom_surjective : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G},
  Function.Surjective Rep.Hom.hom
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.hom_inv_h₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : E.I₀) {Z : C} (h : E.X (e.inv.s₀ (e.hom.s₀ i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.hom.h₀ i) (CategoryTheory.CategoryStruct.comp (e.inv.h₀ (e.hom.s₀ i)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDivInvOneMonoidOfMulOpposite : {M : Type u_1} → [DivInvOneMonoid Mᵐᵒᵖ] → DivInvOneMonoid Mᵈᵐᵃ
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMapZero.nonUnitalStarAlgHom_apply_mul_eq_zero : ∀ {𝕜 : Type u_2} {A : Type u_3} [inst : RCLike 𝕜] [inst_1 : NonUnitalSemiring A] [inst_2 : Star A]
  [inst_3 : TopologicalSpace A] [SeparatelyContinuousMul A] [T2Space A] [inst_6 : DistribMulAction 𝕜 A]
  [IsScalarTower 𝕜 A A] {s : Set 𝕜} [inst_8 : Fact (0 ∈ s)] [CompactSpace ↑s] (φ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A)
  (a : A),
  φ (ContinuousMapZero.id s) * a = 0 →
    φ (star (ContinuousMapZero.id s)) * a = 0 → Continuous ⇑φ → ∀ (f : ContinuousMapZero (↑s) 𝕜), φ f * a = 0
-- Mathlib.Order.Category.Semilat
SemilatInfCat.of.inj : ∀ {X : Type u} {isSemilatticeInf : SemilatticeInf X} {isOrderTop : OrderTop X} {X_1 : Type u}
  {isSemilatticeInf_1 : SemilatticeInf X_1} {isOrderTop_1 : OrderTop X_1},
  { X := X, isSemilatticeInf := isSemilatticeInf, isOrderTop := isOrderTop } =
      { X := X_1, isSemilatticeInf := isSemilatticeInf_1, isOrderTop := isOrderTop_1 } →
    X = X_1 ∧ isSemilatticeInf ≍ isSemilatticeInf_1 ∧ isOrderTop ≍ isOrderTop_1
-- Mathlib.Algebra.Order.Ring.StandardPart
/-- An embedding from an Archimedean field into `K` induces an embedding into
`FiniteResidueField K`.  -/
ArchimedeanClass.FiniteResidueField.ofArchimedean : {K : Type u_1} →
  [inst : LinearOrder K] →
    [inst_1 : Field K] →
      [inst_2 : IsOrderedRing K] →
        {R : Type u_2} →
          [inst_3 : LinearOrder R] →
            [inst_4 : CommRing R] →
              [IsStrictOrderedRing R] → [Archimedean R] → R →+*o K → R →+*o ArchimedeanClass.FiniteResidueField K
-- Mathlib.Algebra.Ring.Parity
Odd.add_one : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Odd a → Even (a + 1)
-- Mathlib.Tactic.Have
/-- The `let` tactic is for adding definitions to the local context of the main goal.
The definition can be unfolded, unlike definitions introduced by `have`.

* `let x : t := e` adds the definition `x : t := e` if `e` is a term of type `t`.
* `let x := e` uses the type of `e` for `t`.
* `let : t := e` and `let := e` use `this` for the name of the hypothesis.
* `let pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that let only one applicable constructor.
  For example, given `p : α × β × γ`, `let ⟨x, y, z⟩ := p` produces the
  local variables `x : α`, `y : β`, and `z : γ`.
* The syntax `let (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `let` term.

## Properties and relations

* Unlike `have`, it is possible to unfold definitions introduced using `let`, using tactics
  such as `simp`, `dsimp`, `unfold`, and `subst`.
* The `clear_value` tactic turns a `let` definition into a `have` definition after the fact.
  The tactic might fail if the local context depends on the value of the variable.
* The `let` tactic is preferred for data (non-propositions).
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
 -/
Mathlib.Tactic.tacticLet_ : Lean.ParserDescr
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.Bool.bif_eq_not_bif : ∀ (d a b c : Bool), ((bif d then a else b) == !bif d then a else c) = (!d && b == !c)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqPoly.beq_spec_3 : ∀ (x x_1 : Lean.Grind.Linarith.Poly),
  (x = Lean.Grind.Linarith.Poly.nil → x_1 = Lean.Grind.Linarith.Poly.nil → False) →
    (∀ (a : ℤ) (a_1 : Lean.Grind.Linarith.Var) (a_2 : Lean.Grind.Linarith.Poly) (b : ℤ) (b_1 : Lean.Grind.Linarith.Var)
        (b_2 : Lean.Grind.Linarith.Poly),
        x = Lean.Grind.Linarith.Poly.add a a_1 a_2 → x_1 = Lean.Grind.Linarith.Poly.add b b_1 b_2 → False) →
      (x == x_1) = false
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.hom_tensorHom : ∀ {R : Type u} [inst : CommSemiring R] {K L M N : SemimoduleCat R} (f : K ⟶ L) (g : M ⟶ N),
  SemimoduleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    TensorProduct.map (SemimoduleCat.Hom.hom f) (SemimoduleCat.Hom.hom g)
-- Mathlib.Topology.Constructible
Topology.IsConstructible.univ : ∀ {X : Type u_2} [inst : TopologicalSpace X], Topology.IsConstructible Set.univ
-- Mathlib.RingTheory.PowerSeries.NoZeroDivisors
PowerSeries.instIsDomain : ∀ {R : Type u_1} [inst : Ring R] [IsDomain R], IsDomain (PowerSeries R)
-- Mathlib.Data.Nat.Fib.Basic
Nat.le_fib_add_one : ∀ (n : ℕ), n ≤ Nat.fib n + 1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- If an expression creates more entries in the stack, for example because it is an application,
then instead of pushing to the stack greedily, we only extend the stack once we need to.
So, the field `previous` is used to extend the `stack` before looking in the `stack`.

For example in `10.add (20.add 30)`, after computing the key `⟨Nat.add, 2⟩`, the stack is still
empty, and `previous` will be `10.add (20.add 30)`.
 -/
Lean.Meta.RefinedDiscrTree.LazyEntry.previous : Lean.Meta.RefinedDiscrTree.LazyEntry → Option Lean.Meta.RefinedDiscrTree.ExprInfo
-- Mathlib.Topology.Algebra.Monoid
/-- Eta-expanded form of `ContinuousWithinAt.pow` -/
ContinuousWithinAt.fun_pow : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Monoid M]
  [ContinuousMul M] {f : X → M} {x : X} {s : Set X},
  ContinuousWithinAt f s x → ∀ (n : ℕ), ContinuousWithinAt (fun i => f i ^ n) s x
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.coe_eq_pi : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), ↑I = Set.univ.pi fun i => Set.Ioc (I.lower i) (I.upper i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry.0.Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (aig : Std.Sat.AIG α) →
        (motive : Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig → Sort u_1) →
          (input : Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig) →
            ((w : ℕ) →
                (lhs rhs : aig.RefVec w) →
                  (cin : aig.Ref) → motive { w := w, vec := { lhs := lhs, rhs := rhs }, cin := cin }) →
              motive input
-- Mathlib.Algebra.Module.Hom
AddMonoid.End.smul_apply : ∀ {R : Type u_1} {A : Type u_4} [inst : Monoid R] [inst_1 : AddCommMonoid A] [inst_2 : DistribMulAction R A] (r : R)
  (f : AddMonoid.End A) (x : A), (r • f) x = r • f x
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.coe_copy : ∀ {α : 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) = f'
-- Std.Sync.Notify
/-- The central state structure for a `Notify`.
 -/
Std.Notify.State : Type
-- Init.Core
/-- The axiom `ofReduceBool` is used to perform proofs by reflection. See `reduceBool`.

This axiom is usually not used directly, because it has some syntactic restrictions.
Instead, the `native_decide` tactic can be used to prove any proposition whose
decidability instance can be evaluated to `true` using the lean compiler / interpreter.

Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
external type checkers that do not implement this feature.
Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
So, you are mainly losing the capability of type checking your development using external checkers.
 -/
Lean.ofReduceBool : ∀ (a b : Bool), Lean.reduceBool a = b → a = b
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_map_left_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.toArrowArrowFunctor.map φ).left.right = φ.τ₃
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Preimage of a non-unital star subalgebra under a non-unital star algebra homomorphism.  -/
NonUnitalStarSubalgebra.comap : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : Module R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] →
                        [NonUnitalAlgHomClass F R A B] →
                          [StarHomClass F A B] → F → NonUnitalStarSubalgebra R B → NonUnitalStarSubalgebra R A
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Measure.setIntegral_compProd : ∀ {α : Type u_5} {β : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {E : Type u_8}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set α},
  MeasurableSet s →
    ∀ {t : Set β},
      MeasurableSet t →
        ∀ {f : α × β → E},
          MeasureTheory.IntegrableOn f (s ×ˢ t) (μ.compProd κ) →
            ∫ (x : α × β) in s ×ˢ t, f x ∂μ.compProd κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ
-- Mathlib.Logic.Function.Conjugate
/-- Any self-map commutes with the identity map.  -/
Function.Commute.id_right : ∀ {α : Type u_1} {f : α → α}, Function.Commute f id
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.IsFiniteKernel.prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ]
  (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsFiniteKernel η], ProbabilityTheory.IsFiniteKernel (κ.prod η)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (sz : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (sz : ℕ) →
      (k : α) →
        (v : β k) → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner sz k v l r)),
  (match Std.DTreeMap.Internal.Impl.inner sz k v l r with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner sz k v l r => h_2 sz k v l r) =
    h_2 sz k v l r
-- Mathlib.Data.Fin.VecNotation
Matrix.const_fin1_eq : ∀ {α : Type u} (x : α), (fun x_1 => x) = ![x]
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_subset_toFinset : ∀ {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite}, hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.Equiv.quotMk_eq_iff : ∀ {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : LawfulMonad m] (ita itb : Std.BundledIterM m β),
  Quot.mk (Std.BundledIterM.Equiv m β) ita = Quot.mk (Std.BundledIterM.Equiv m β) itb ↔
    Std.BundledIterM.Equiv m β ita itb
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.instInhabited : {𝕜 : 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] → Inhabited (P →ᵃⁱ[𝕜] P)
-- Mathlib.GroupTheory.MonoidLocalization.Away
AddLocalization.Away.addMonoidOf.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (x : M),
  AddLocalization.Away.addMonoidOf x = AddLocalization.addMonoidOf (AddSubmonoid.multiples x)
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.support_expand_subset : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {p : ℕ} (φ : MvPolynomial σ R) [inst_1 : DecidableEq σ],
  ((MvPolynomial.expand p) φ).support ⊆ Finset.image (fun x => p • x) φ.support
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, (m.insertIfNew k v).isEmpty = false
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestMatchAt_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt p pos pos' ↔
    ∃ (h : pos ≠ s.endPos), pos' = pos.next h ∧ p (pos.get h) = true
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₃_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (β : CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip)
  (X Y Z : C),
  (((CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₃ β).app X).app Y).app Z =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight ((β.hom.app X).app Z) Y
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.instPartialOrder : {X : Type u_2} → [inst : TopologicalSpace X] → PartialOrder (DiscreteQuotient X)
-- Mathlib.NumberTheory.RamificationInertia.Inertia
Ideal.absNorm_eq_pow_inertiaDeg'_of_liesOver : ∀ {R : Type u} [inst : CommRing R] {S : Type u_1} [inst_1 : CommRing S] [inst_2 : IsDedekindDomain S]
  [inst_3 : Module.Free ℤ S] [inst_4 : IsDedekindDomain R] [inst_5 : Module.Free ℤ R] [inst_6 : Algebra S R]
  [Module.Finite S R] (P : Ideal R) (p : Ideal S) [P.LiesOver p],
  p.IsPrime → p ≠ ⊥ → Ideal.absNorm P = Ideal.absNorm p ^ p.inertiaDeg' P
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false},
  t.max he ∈ t
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zero_mem_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] {s : Set α} {n : ℕ}, 0 ∈ s → 0 ∈ n • s
-- Mathlib.Data.String.Basic
String.ltb_cons_addChar' : ∀ (c : Char) (s₁ s₂ : String.Legacy.Iterator),
  String.ltb { s := String.ofList (c :: s₁.s.toList), i := s₁.i + c }
      { s := String.ofList (c :: s₂.s.toList), i := s₂.i + c } =
    String.ltb s₁ s₂
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.Functor C V} [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  {F' G' : CategoryTheory.Functor C V} [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F' G'] (f : F ⟶ F')
  (g : G ⟶ G') (x y : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
      ((CategoryTheory.MonoidalCategory.DayConvolution.map f g).app
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app x) (g.app y))
      ((CategoryTheory.MonoidalCategory.DayConvolution.unit F' G').app (x, y))
-- Mathlib.Combinatorics.SetFamily.Intersecting
/-- Every family of finite sets is `univ`-intersecting.
 -/
Set.IsIntersectingOf.univ : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Set (Finset α)}, Set.univ.IsIntersectingOf 𝒜
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey! =
    t.minKey?.elim k fun k' => if (compare k k').isLE = true then k else k'
-- Mathlib.Probability.Process.Stopping
MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_range : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {μ : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration ι m} {τ : Ω → WithTop ι} {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} [MeasureTheory.SigmaFiniteFiltration μ ℱ]
  (hτ : MeasureTheory.IsStoppingTime ℱ τ),
  (Set.range τ).Countable →
    ∀ [MeasureTheory.SigmaFinite (μ.trim ⋯)] (i : ι),
      μ[f | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] μ[f | ↑ℱ i]
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instInhabited : (k : Type u_1) → [inst : Field k] → Inhabited (AlgebraicClosure k)
-- Mathlib.Tactic.Linarith.Verification
/-- `addNegEqProofsIdx l` inspects a list `l` of pairs `(h, i)` where `h` proves
`tᵢ Rᵢ 0` and `i` records the original index of the hypothesis. For each
equality proof `t = 0` in the list, it appends a proof of `-t = 0` with the
same index `i`. All other entries are preserved.
 -/
Mathlib.Tactic.Linarith.addNegEqProofsIdx : List (Lean.Expr × ℕ) → Lean.MetaM (List (Lean.Expr × ℕ))
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of two `C^n` functions within a set at a point is `C^n` within this
set at this point.  -/
ContDiffWithinAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {n : WithTop ℕ∞} {𝕜' : Type u_3} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {s : Set E} {f : E → 𝕜'} {g : E → F},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n (f • g) s x
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `thirdToMax₃ j₁ j₂ j₃` is an arbitrary choice of morphism from `j₃` to `max₃ j₁ j₂ j₃`,
whose existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.thirdToMax₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] → (j₁ j₂ j₃ : C) → j₃ ⟶ CategoryTheory.IsFiltered.max₃ j₁ j₂ j₃
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHSubOffset_5 : HSub Std.Time.Timestamp Std.Time.Millisecond.Offset Std.Time.Timestamp
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMapLiftEquiv.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (n m k : ℕ)
  (hn : n = m + k) (p : Polynomial.MonicDegreeEq S n),
  MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn p =
    {
      toFun := fun f =>
        ⟨((MvPolynomial.mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
            (MvPolynomial.mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
          ⋯⟩,
      invFun := fun q =>
        ⟨Algebra.TensorProduct.lift ((MvPolynomial.mapEquivMonic R S m).symm (↑q).1)
            ((MvPolynomial.mapEquivMonic R S k).symm (↑q).2) ⋯,
          ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateUsetImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.FVarId → ℕ → Lean.FVarId → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvironmentHeader.moduleName2Idx : Lean.EnvironmentHeader → Std.HashMap Lean.Name Lean.ModuleIdx
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.nil : Tactic.ComputeAsymptotics.BasisExtension []