mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Fintype.piFinset_smul : ∀ {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (β i)] [inst_3 : (i : ι) → SMul (α i) (β i)] (s : (i : ι) → Finset (α i))
  (t : (i : ι) → Finset (β i)), (Fintype.piFinset fun i => s i • t i) = Fintype.piFinset s • Fintype.piFinset t
-- Mathlib.Topology.UrysohnsLemma
/-- An auxiliary type for the proof of Urysohn's lemma: a pair of a closed set `C` and its open
neighborhood `U`, together with the assumption that `C` and `U` satisfy the property `P C U`.
The latter assumption will make it possible to prove simultaneously both versions of Urysohn's
lemma, in normal spaces (with `P` always true) and in locally compact spaces
(with `P C U = IsCompact C`). We put also in the structure the assumption that, for any such pair,
one may find an intermediate pair in between satisfying `P`,
to avoid carrying it around in the argument.
 -/
Urysohns.CU : {X : Type u_2} → [TopologicalSpace X] → (Set X → Set X → Prop) → Type u_2
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- The scalar product along the fibers of the bundle.  -/
Bundle.ContMDiffRiemannianMetric.inner : {EB : Type u_1} →
  [inst : NormedAddCommGroup EB] →
    [inst_1 : NormedSpace ℝ EB] →
      {HB : Type u_2} →
        [inst_2 : TopologicalSpace HB] →
          {IB : ModelWithCorners ℝ EB HB} →
            {n : WithTop ℕ∞} →
              {B : Type u_3} →
                [inst_3 : TopologicalSpace B] →
                  [inst_4 : ChartedSpace HB B] →
                    {F : Type u_4} →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace ℝ F] →
                          {E : B → Type u_5} →
                            [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] →
                              [inst_8 : (b : B) → TopologicalSpace (E b)] →
                                [inst_9 : (b : B) → AddCommGroup (E b)] →
                                  [inst_10 : (b : B) → Module ℝ (E b)] →
                                    [inst_11 : FiberBundle F E] →
                                      [inst_12 : VectorBundle ℝ F E] →
                                        Bundle.ContMDiffRiemannianMetric IB n F E → (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- `X` is terminal if the cone it induces on the empty diagram is limiting.  -/
CategoryTheory.Limits.IsTerminal : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Type (max (max 0 u₁) v₁)
-- Init.Data.Char.Lemmas
Char.le_antisymm : ∀ {a b : Char}, a ≤ b → b ≤ a → a = b
-- Mathlib.Tactic.Linter.MinImports
/-- The `minImports` linter incrementally computes the minimal imports needed for each file to build.
Whenever it detects that a new command requires an increase in the (transitive) imports that it
computed so far, it emits a warning mentioning the bigger minimal imports.

Unlike the related `#min_imports` command, the linter takes into account notation and tactic
information.
It also works incrementally, providing information that is better suited, for instance, to split
files.

Another important difference is that the `minImports` *linter* starts counting imports from
where the option is set to `true` *downwards*, whereas the `#min_imports` *command* looks at the
imports needed from the command *upwards*.
 -/
Mathlib.Linter.MinImports.«command#import_bumps» : Lean.ParserDescr
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.subtype_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : SetLike S R] [hSR : SubringClass S R] {s : S} (x : ↥s),
  (SubringClass.subtype s) x = ↑x
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_fst : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}, Measurable Prod.fst
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidalFunctor_ε : ∀ {M : Type u} [inst : Monoid M] {N : Type u'} [inst_1 : Monoid N] (F : M →* N),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Discrete.monoidalFunctor F) = CategoryTheory.Discrete.eqToHom ⋯
-- Mathlib.Probability.Martingale.Upcrossing
/-- `upcrossingStrat a b f N n` is 1 if `n` is between a consecutive pair of lower and upper
crossings and is 0 otherwise. `upcrossingStrat` is shifted by one index so that it is adapted
rather than predictable.  -/
MeasureTheory.upcrossingStrat : {Ω : Type u_1} → ℝ → ℝ → (ℕ → Ω → ℝ) → ℕ → ℕ → Ω → ℝ
-- Init.Data.String.Slice
String.Slice.instInhabitedRevSplitIterator : {a : String.Slice → Type} →
  {a_1 : Type} →
    {a_2 : a_1} →
      {a_3 : String.Slice} →
        {a_4 : String.Slice.Pattern.ToBackwardSearcher a_2 a} → Inhabited (String.Slice.RevSplitIterator a_2 a_3)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.ext : ∀ {M N : SemiNormedGrp} {f₁ f₂ : M ⟶ N},
  (∀ (x : M.carrier), (CategoryTheory.ConcreteCategory.hom f₁) x = (CategoryTheory.ConcreteCategory.hom f₂) x) → f₁ = f₂
-- Lean.Meta.LazyDiscrTree
/-- Returns true iff the argument should be treated as a "wildcard" by the
discrimination tree.

This includes proofs, instance implicit arguments, implicit arguments,
and terms of the form `noIndexing t`

This is a clone of `Lean.Meta.DiscrTree.ignoreArg` and mainly added to
avoid coupling between `DiscrTree` and `LazyDiscrTree` while both are
potentially subject to independent changes.
 -/
Lean.Meta.LazyDiscrTree.MatchClone.ignoreArg : Lean.Expr → ℕ → Array Lean.Meta.ParamInfo → Lean.MetaM Bool
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.includeRight_lid : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_11}
  [inst_3 : Semiring S] [inst_4 : Algebra R S] (m : TensorProduct R R M),
  1 ⊗ₜ[R] (TensorProduct.lid R M) m = (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap) m
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_coe_mem_lie : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : LieSubmodule R L M} [inst_5 : LieAlgebra R L]
  {I : LieIdeal R L} (x : ↥I) (m : ↥N), ⁅↑x, ↑m⁆ ∈ ⁅I, N⁆
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mono_nonneg : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [inst_1 : Lattice β] [HasSolidNorm β] [AddLeftMono β] {f g : α → β},
  MeasureTheory.Integrable g μ →
    MeasureTheory.AEStronglyMeasurable f μ →
      (∀ᵐ (a : α) ∂μ, 0 ≤ f a) → (∀ᵐ (a : α) ∂μ, f a ≤ g a) → MeasureTheory.Integrable f μ
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.invFun_eq_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  {f : α ≃+o β}, f.invFun = ⇑f.symm
-- Init.Tactics
/-- If true (default: false), then use only kernel reduction when reducing the `Decidable` instance.
This is more efficient, since the default mode reduces twice (once in the elaborator and again in the kernel),
however kernel reduction ignores transparency settings.  -/
Lean.Parser.Tactic.DecideConfig.kernel : Lean.Parser.Tactic.DecideConfig → Bool
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_eq_zero : ∀ {r : ENNReal}, ⌈r⌉ₑ = 0 ↔ r = 0
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {ι : Type u_2} {c : ComplexShape ι} {Hₚ : ι → CategoryTheory.Functor TopPair C}
  {H : ι → CategoryTheory.Functor TopCat C} {iso : (i : ι) → H i ≅ TopPair.incl.comp (Hₚ i)}
  {δ : (i j : ι) → Hₚ i ⟶ TopPair.proj₂.comp (H j)}
  {shape_δ : autoParam (∀ (i j : ι), ¬c.Rel i j → δ i j = 0) TopPair.HomologyPretheory.shape_δ._autoParam}
  {Hₚ_1 : ι → CategoryTheory.Functor TopPair C} {H_1 : ι → CategoryTheory.Functor TopCat C}
  {iso_1 : (i : ι) → H_1 i ≅ TopPair.incl.comp (Hₚ_1 i)} {δ_1 : (i j : ι) → Hₚ_1 i ⟶ TopPair.proj₂.comp (H_1 j)}
  {shape_δ_1 : autoParam (∀ (i j : ι), ¬c.Rel i j → δ_1 i j = 0) TopPair.HomologyPretheory.shape_δ._autoParam},
  { Hₚ := Hₚ, H := H, iso := iso, δ := δ, shape_δ := shape_δ } =
      { Hₚ := Hₚ_1, H := H_1, iso := iso_1, δ := δ_1, shape_δ := shape_δ_1 } →
    Hₚ = Hₚ_1 ∧ H = H_1 ∧ iso ≍ iso_1 ∧ δ ≍ δ_1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.instEntailsPosFin : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.Entails (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
    (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
-- Mathlib.MeasureTheory.Function.EssSup
essSup_const_bot : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : CompleteLattice β],
  essSup (fun x => ⊥) μ = ⊥
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.restrict₀_range_eq_top : ∀ {A : Type u_1} {B : Type u_2} [inst : GroupWithZero A] [inst_1 : GroupWithZero B] (f : A →*₀ B),
  Set.range ⇑(MonoidWithZeroHom.ValueGroup₀.restrict₀ f) = ⊤
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_of_one_lt_sumInv : ∀ {p q r : ℕ+}, 1 < ADEInequality.sumInv {p, q, r} → ADEInequality.Admissible {p, q, r}
-- Mathlib.Data.Matrix.DMatrix
DMatrix.neg_apply : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [inst : (i : m) → (j : n) → Neg (α i j)] (M : DMatrix m n α)
  (i : m) (j : n), (-M) i j = -M i j
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedCommGroup.mk : {E : Type u_8} →
  [toNorm : Norm E] →
    [toCommGroup : CommGroup E] →
      [toPseudoMetricSpace : PseudoMetricSpace E] →
        autoParam (∀ (x y : E), dist x y = ‖x⁻¹ * y‖) SeminormedCommGroup.dist_eq._autoParam → SeminormedCommGroup E
-- Init.Data.Array.Lex.Lemmas
Array.lt_trans : ∀ {α : Type u_1} [inst : LT α] [i₁ : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2]
  {xs ys zs : Array α}, xs < ys → ys < zs → xs < zs
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (M : ↑(F.obj { as := Opposite.op S }).obj) (i : ι),
  ((F.toDescentDataAsCoalgebra f).obj M).obj i = (F.map (f i).op.toLoc).l.toFunctor.obj M
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
OrderDual.instDistribMulAction : {G₀ : Type u_1} →
  {M₀ : Type u_2} → [inst : Monoid G₀] → [inst_1 : AddMonoid M₀] → [DistribMulAction G₀ M₀] → DistribMulAction G₀ᵒᵈ M₀
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.instFinite : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad n] [inst_1 : Std.Iterator α m β]
  {lift : ⦃α : Type w⦄ → m α → n α} {f : β → Std.Iterators.PostconditionT n (Option γ)} [Std.Iterators.Finite α m],
  Std.Iterators.Finite (Std.Iterators.Types.FilterMap α m n lift f) n
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.codRestrict_le : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.PartialEquiv M N) {A : L.Substructure N} (h : A ≤ f.cod), f.codRestrict h ≤ f
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.eq_of_apply_eq_iff : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {b₁ b₂ : Module.Basis ι R M}, b₁ = b₂ ↔ ∀ (i : ι), b₁ i = b₂ i
-- Mathlib.Data.Finset.Slice
/-- Elements in distinct slices must be distinct.  -/
Finset.ne_of_mem_slice : ∀ {α : Type u_1} {𝒜 : Finset (Finset α)} {A₁ A₂ : Finset α} {r₁ r₂ : ℕ},
  A₁ ∈ 𝒜.slice r₁ → A₂ ∈ 𝒜.slice r₂ → r₁ ≠ r₂ → A₁ ≠ A₂
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.mk.injEq : ∀ (declName : Lean.Name) (levelParams : List Lean.Name) (type value : Lean.Expr) (declNames : Array Lean.Name)
  (declNameNonRec : Lean.Name) (argsPacker : Lean.Meta.ArgsPacker) (fixedParamPerms : Lean.Elab.FixedParamPerms)
  (declName_1 : Lean.Name) (levelParams_1 : List Lean.Name) (type_1 value_1 : Lean.Expr) (declNames_1 : Array Lean.Name)
  (declNameNonRec_1 : Lean.Name) (argsPacker_1 : Lean.Meta.ArgsPacker) (fixedParamPerms_1 : Lean.Elab.FixedParamPerms),
  ({ declName := declName, levelParams := levelParams, type := type, value := value, declNames := declNames,
        declNameNonRec := declNameNonRec, argsPacker := argsPacker, fixedParamPerms := fixedParamPerms } =
      { declName := declName_1, levelParams := levelParams_1, type := type_1, value := value_1,
        declNames := declNames_1, declNameNonRec := declNameNonRec_1, argsPacker := argsPacker_1,
        fixedParamPerms := fixedParamPerms_1 }) =
    (declName = declName_1 ∧
      levelParams = levelParams_1 ∧
        type = type_1 ∧
          value = value_1 ∧
            declNames = declNames_1 ∧
              declNameNonRec = declNameNonRec_1 ∧ argsPacker = argsPacker_1 ∧ fixedParamPerms = fixedParamPerms_1)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst Y Z) h)
-- Init.Prelude
/-- (Boolean) equality comparator for names.  -/
Lean.Name.beq : Lean.Name → Lean.Name → Bool
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.ExprWithAnchor.e : Lean.Meta.Grind.ExprWithAnchor → Lean.Expr
-- Mathlib.Data.Rat.Cast.Defs
Rat.subsingleton_ringHom : ∀ {R : Type u_5} [inst : Semiring R], Subsingleton (ℚ →+* R)
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.fromThinSkeleton_isEquivalence : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : Quiver.IsThin C],
  (CategoryTheory.ThinSkeleton.fromThinSkeleton C).IsEquivalence
-- Mathlib.Analysis.Calculus.Implicit
/-- Any point in some neighborhood of `a` can be represented as
`HasStrictFDerivAt.implicitFunctionOfComplemented` of some point.  -/
HasStrictFDerivAt.eq_implicitFunctionOfComplemented : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented),
  ∀ᶠ (x : E) in nhds a,
    HasStrictFDerivAt.implicitFunctionOfComplemented f f' hf hf' hker (f x)
        (↑(HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) x).2 =
      x
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.tendsto_zero_of_norm_tendsto_zero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {ncs : CauSeq ℤ_[p] norm} {F : Polynomial R},
  Filter.Tendsto (fun i => ‖(Polynomial.aeval (↑ncs i)) F‖) Filter.atTop (nhds 0) →
    Filter.Tendsto (fun i => (Polynomial.aeval (↑ncs i)) F) Filter.atTop (nhds 0)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_finsetSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_4} {f : ι → TopologicalSpace.CompactOpens α} {s : Finset ι},
  ↑(s.sup f) = ⋃ i ∈ s, ↑(f i)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.mk_eq_mk : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f : CauSeq β abv), ⟦f⟧ = CauSeq.Completion.mk f
-- Mathlib.SetTheory.Cardinal.ENat
/-- **Alias** of the reverse direction of `Cardinal.ofENat_toENat_eq_self`. -/
Cardinal.ofENat_toENat : ∀ {a : Cardinal.{u_1}}, a ≤ Cardinal.aleph0 → ↑(Cardinal.toENat a) = a
-- Init.MetaTypes
/-- A neutral configuration for `simp`, turning off all reductions and other built-in simplifications.
 -/
Lean.Meta.Simp.neutralConfig : Lean.Meta.Simp.Config
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.modifyKey_eq_alterKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] (k : α) (f : β → β) (l : List ((_ : α) × β)),
  Std.Internal.List.Const.modifyKey k f l = Std.Internal.List.Const.alterKey k (fun x => Option.map f x) l
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertYear : Std.Time.Year → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.instIsRightCancelMulZeroOfIsLeftCancelMulZero : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [IsLeftCancelMulZero α], IsRightCancelMulZero αᵐᵒᵖ
-- Batteries.Tactic.Alias
/-- Plain alias  -/
Batteries.Tactic.Alias.AliasInfo.plain : Lean.Name → Batteries.Tactic.Alias.AliasInfo
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is algebraic, then an intermediate field of `E / F` contains the
separable closure of `F` in `E` if and only if `E` is purely inseparable over it.  -/
separableClosure_le_iff : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E]
  (L : IntermediateField F E), separableClosure F E ≤ L ↔ IsPurelyInseparable (↥L) E
-- Mathlib.Algebra.Tropical.Lattice
instSupSetTropical : {R : Type u_1} → [SupSet R] → SupSet (Tropical R)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.mk.inj : ∀ {M : Type u_1} {inst : Monoid M} {N : Type u_2} {inst_1 : Monoid N} {φ : M →* N} {A : Type u_10}
  {inst_2 : AddMonoid A} {inst_3 : DistribMulAction M A} {B : Type u_11} {inst_4 : AddMonoid B}
  {inst_5 : DistribMulAction N B} {toMulActionHom : A →ₑ[⇑φ] B} {map_zero' : toMulActionHom.toFun 0 = 0}
  {map_add' : ∀ (x y : A), toMulActionHom.toFun (x + y) = toMulActionHom.toFun x + toMulActionHom.toFun y}
  {toMulActionHom_1 : A →ₑ[⇑φ] B} {map_zero'_1 : toMulActionHom_1.toFun 0 = 0}
  {map_add'_1 : ∀ (x y : A), toMulActionHom_1.toFun (x + y) = toMulActionHom_1.toFun x + toMulActionHom_1.toFun y},
  { toMulActionHom := toMulActionHom, map_zero' := map_zero', map_add' := map_add' } =
      { toMulActionHom := toMulActionHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 } →
    toMulActionHom = toMulActionHom_1
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.mk.sizeOf_spec : ∀ {X : Type u_4} [inst : TopologicalSpace X] [inst_1 : SizeOf X] (toFun : ℕ → Set X)
  (isCompact' : ∀ (n : ℕ), IsCompact (toFun n)) (subset_interior_succ' : ∀ (n : ℕ), toFun n ⊆ interior (toFun (n + 1)))
  (iUnion_eq' : ⋃ n, toFun n = Set.univ),
  sizeOf
      { toFun := toFun, isCompact' := isCompact', subset_interior_succ' := subset_interior_succ',
        iUnion_eq' := iUnion_eq' } =
    1 + sizeOf iUnion_eq'
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_add_right' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {g : α → ENNReal},
  AEMeasurable g μ → ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.instHasReverseSymmetrify : {V : Type u_2} → [inst : Quiver V] → Quiver.HasReverse (Quiver.Symmetrify V)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.RankLeOneStruct.mk.injEq : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (emb : ValuativeRel.ValueGroupWithZero R →*₀ NNReal)
  (strictMono : StrictMono ⇑emb) (emb_1 : ValuativeRel.ValueGroupWithZero R →*₀ NNReal)
  (strictMono_1 : StrictMono ⇑emb_1),
  ({ emb := emb, strictMono := strictMono } = { emb := emb_1, strictMono := strictMono_1 }) = (emb = emb_1)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_div : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {𝕜 : Type u_8} [inst : RCLike 𝕜] (r : 𝕜) (f : ℝ → 𝕜),
  ∫ (x : ℝ) in a..b, f x / r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) / r
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.mkPartialTermInfo : Lean.Name →
  Lean.Syntax →
    optParam (Option Lean.Expr) none → optParam (Option Lean.LocalContext) none → Lean.Elab.TermElabM Lean.Elab.Info
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- If `v` is a family of vectors of `M` indexed by a linearly ordered type, then the span of the
range of `exteriorPower.ιMulti_family R n v`, i.e., of the family of `n`-fold exterior products
of elements of `v`, is the image of the map of exterior powers induced by the inclusion of
the span of `v` into `M`.  -/
exteriorPower.ιMulti_family_span : ∀ (R : Type u) [inst : CommRing R] {n : ℕ} {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Type u_4}
  [inst_3 : LinearOrder I] (v : I → M),
  (exteriorPower.map n (Submodule.span R (Set.range v)).subtype).range =
    Submodule.span R (Set.range (exteriorPower.ιMulti_family R n v))
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.hasForgetToBipointed : CategoryTheory.HasForget₂ TwoP Bipointed
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.add_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Add β]
  [inst_3 : ContinuousAdd β] (f g : C(α, β)) (x : α), (f + g) x = f x + g x
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of the reverse direction of `Finset.le_inf'_iff`. -/
Finset.le_inf' : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α},
  (∀ b ∈ s, a ≤ f b) → a ≤ s.inf' H f
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_8 : HSub Std.Time.Millisecond.Offset Std.Time.Minute.Offset Std.Time.Millisecond.Offset
-- Mathlib.Data.Seq.Basic
Stream'.Seq.drop.eq_2 : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ), s.drop n.succ = (s.drop n).tail
-- Mathlib.Order.Iterate
Function.Commute.iterate_pos_le_iff_map_le' : ∀ {α : Type u_1} [inst : LinearOrder α] {f g : α → α},
  Function.Commute f g → StrictMono f → Monotone g → ∀ {x : α} {n : ℕ}, 0 < n → (f^[n] x ≤ g^[n] x ↔ f x ≤ g x)
-- Init.Prelude
Lean.PrettyPrinter.instMonadQuotationUnexpandM : Lean.MonadQuotation Lean.PrettyPrinter.UnexpandM
-- Mathlib.RingTheory.Valuation.Integers
Valuation.leSubmodule_v_le_of_mem : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [inst_1 : Field K] (v : Valuation K Γ₀)
  {S : Submodule (↥v.integer) K} {x : K}, x ∈ S → v.leSubmodule (v x) ≤ S
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- `ContinuousLinearMap.inr` has a continuous left inverse.  -/
ContinuousLinearMap.HasLeftInverse.inr : ∀ {R : Type u_1} [inst : Semiring R] {F : Type u_4} {G : Type u_6} [inst_1 : TopologicalSpace F]
  [inst_2 : AddCommMonoid F] [inst_3 : Module R F] [inst_4 : TopologicalSpace G] [inst_5 : AddCommMonoid G]
  [inst_6 : Module R G], (ContinuousLinearMap.inr R F G).HasLeftInverse
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_const_zero : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A),
  cfc (fun x => 0) a = 0
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.eraseIdx.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (head : α) (as : List α) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (head : α) → (as : List α) → motive (head :: as) 0)
  (h_3 : (a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ),
  (match head :: as, 0 with
    | [], x => h_1 x
    | head :: as, 0 => h_2 head as
    | a :: as, n.succ => h_3 a as n) =
    h_2 head as