mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.tprod_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α]
  [CompleteSpace α] [T0Space α] {f : β → γ → α},
  Multipliable (Function.uncurry f) → ∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.isScalarTower' : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  IsScalarTower R (TensorProduct R S S) Ω[S⁄R]
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.getKey? (t.minKey he) = some (t.minKey he)
-- Mathlib.Topology.Order.Compact
atBot_le_cocompact : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [NoMinOrder α] [ClosedIicTopology α],
  Filter.atBot ≤ Filter.cocompact α
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instFullHoCatToHoCat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  HomotopicalAlgebra.BifibrantObject.toHoCat.Full
-- Mathlib.Data.Finset.Max
Finset.min_erase_ne_self : ∀ {α : Type u_2} [inst : LinearOrder α] {x : α} {s : Finset α}, (s.erase x).min ≠ ↑x
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
/-- The entropy of `T` restricted to `F`, obtained by taking the supremum
of `coverEntropyEntourage` over entourages. Note that this supremum is approached by taking small
entourages. This first version uses a `limsup`, and is chosen as the default definition
for topological entropy.  -/
Dynamics.coverEntropy : {X : Type u_1} → [UniformSpace X] → (X → X) → Set X → EReal
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.integral_normed : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure], ∫ (x : E), f.normed μ x ∂μ = 1
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.iff_flat_and_lTensor_reflects_triviality : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔
    Module.Flat R M ∧
      ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N],
        Subsingleton (TensorProduct R M N) → Subsingleton N
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVLogicalExpr.Sat : Std.Tactic.BVDecide.BVLogicalExpr → Std.Tactic.BVDecide.BVExpr.Assignment → Prop
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- `@[simp]`-normal form of `pushforward_map_app_apply`.  -/
PresheafOfModules.pushforward_map_app_apply' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) {M N : PresheafOfModules R} (α : M ⟶ N) (X : Cᵒᵖ)
  (m : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))),
  (ModuleCat.Hom.hom (((PresheafOfModules.pushforward φ).map α).app X)) m =
    (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op (F.obj (Opposite.unop X))))) m
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.instNormalSubtypeMemSubgroupStabilizerInertia : ∀ {M : Type u_1} [inst : Group M] {R : Type u_4} [inst_1 : Ring R] (P : Ideal R) [inst_2 : MulSemiringAction M R],
  (Ideal.inertia (↥(MulAction.stabilizer M P)) P).Normal
-- Std.Sync.Broadcast
/-- Unsubscribes a `Receiver` from the `Bounded` channel.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.unsubscribe : {α : Type} → Std.Bounded.Receiver✝ α → IO Unit
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (size : ℕ) (k : α)
  (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) =
    h_2 size k v r
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.Localization.exists_leftFraction₃ : ∀ {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 : L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C}
  (f f' f'' : L.obj X ⟶ L.obj Y), ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)}, m.WF → k ∈ m → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
TopCat.Sheaf.eq_app_of_locally_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat}
  {F : TopCat.Sheaf C X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens ↑X} {V : TopologicalSpace.Opens ↑X}
  {G : TopCat.Sheaf C X} {f : F ⟶ G} {s : CategoryTheory.ToType (F.obj.obj (Opposite.op (iSup U)))}
  {t : CategoryTheory.ToType (G.obj.obj (Opposite.op V))}
  {sf : (i : ι) → CategoryTheory.ToType (F.obj.obj (Opposite.op (U i)))},
  TopCat.Presheaf.IsGluing F.obj U sf s →
    ∀ (hV : ∀ (i : ι), U i ≤ V),
      (∀ (i : ι),
          (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op (U i)))) (sf i) =
            (CategoryTheory.ConcreteCategory.hom (G.obj.map (CategoryTheory.homOfLE ⋯).op)) t) →
        (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op (iSup U)))) s =
          (CategoryTheory.ConcreteCategory.hom (G.obj.map (CategoryTheory.homOfLE ⋯).op)) t
-- Lean.Exception
/-- Increment the current recursion depth and then execute `x`.
Throw an exception if maximum recursion depth has been reached.
We use this combinator to prevent stack overflows.
 -/
Lean.withIncRecDepth : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → [Lean.MonadRecDepth m] → m α → m α
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- The matrix of `toSpanSingleton R M₂ x` given by bases `v₁` and `v₂` is equal to
`vecMulVec (v₂.repr x) v₁`. When `v₁ = Module.Basis.singleton`
then this is the column matrix of `v₂.repr x`.  -/
LinearMap.toMatrix_toSpanSingleton : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {M₂ : Type u_6} [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] [inst_5 : Finite m] (v₁ : Module.Basis n R R)
  (v₂ : Module.Basis m R M₂) (x : M₂),
  (LinearMap.toMatrix v₁ v₂) (LinearMap.toSpanSingleton R M₂ x) = Matrix.vecMulVec ⇑(v₂.repr x) ⇑v₁
-- Mathlib.Analysis.Convex.Combination
Set.Finite.convexHull_eq : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {s : Set E} (hs : s.Finite),
  (convexHull R) s = {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ hs.toFinset, w y = 1 ∧ hs.toFinset.centerMass w id = x}
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.thmNs : Lean.ParserDescr
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
QuadraticMap.IsometryEquiv.map_posDef_iff : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : AddCommGroup M] [inst_1 : AddCommGroup M'] [inst_2 : CommRing R]
  [inst_3 : LinearOrder R] [inst_4 : Module R M] {Q : QuadraticForm R M} [inst_5 : Module R M']
  {Q' : QuadraticForm R M'} {V : Submodule R M} (e : QuadraticMap.IsometryEquiv Q Q'),
  (QuadraticMap.restrict Q' (Submodule.map (↑e.toLinearEquiv) V)).PosDef ↔ (QuadraticMap.restrict Q V).PosDef
-- Std.Internal.Parsec.ByteArray
/-- Parse one or more ASCII digits into a `Nat`.
 -/
Std.Internal.Parsec.ByteArray.digits : Std.Internal.Parsec.ByteArray.Parser ℕ
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.coe_eval : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ), ⇑(AdicCompletion.eval I M n) = fun f => ↑f n
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.State.mctx : Lean.MetavarContext.MkBinding.State → Lean.MetavarContext
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.AttributeEntry.mk : {γ : Type} → Lean.KeyedDeclsAttribute.OLeanEntry → Bool → γ → Lean.KeyedDeclsAttribute.AttributeEntry γ
-- Mathlib.Order.Interval.Finset.Basic
/-- `Finset.cons` version of `Finset.Ioo_insert_left`.  -/
Finset.Ico_eq_cons_Ioo : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
  a < b → Finset.Ico a b = Finset.cons a (Finset.Ioo a b) ⋯
-- Lean.Elab.MutualInductive
/-- Syntax for the name of the constructor, used to apply terminfo. If the source is synthetic, terminfo is not applied.  -/
Lean.Elab.Command.CtorView.declId : Lean.Elab.Command.CtorView → Lean.Syntax
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trNormal.eq_4 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trNormal (Turing.TM2.Stmt.load a q) = Turing.TM1.Stmt.load (fun x => a) (Turing.TM2to1.trNormal q)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.instUnique : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [Subsingleton M] → Unique (PolynomialModule R M)
-- Mathlib.Algebra.Order.Field.Basic
le_div_iff_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → (a ≤ b / c ↔ b ≤ a * c)
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.AbelianStruct.ι_imageπ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {f : X ⟶ Y} (self : CategoryTheory.Abelian.AbelianStruct f) {Z : C} (h : self.image ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι self.kernelFork)
      (CategoryTheory.CategoryStruct.comp self.imageπ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Sym.Lemmas
Lean.Sym.Int64.lt_eq_true : ∀ (a b : Int64), decide (a < b) = true → (a < b) = True
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.id_onRelation : ∀ (L : FirstOrder.Language) (_n : ℕ) (a : L.Relations _n), (FirstOrder.Language.LHom.id L).onRelation a = id a
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator'_zpowers_eq_top : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [inst_2 : v.IsRankOneDiscrete], Subgroup.zpowers (Valuation.IsRankOneDiscrete.generator' v) = ⊤
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableWithinAt.neg` -/
DifferentiableWithinAt.fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (fun i => -f i) s x
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.isCofiltered_costructuredArrow_of_isCofiltered_of_exists : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] (d : D),
  (∃ c, Nonempty (F.obj c ⟶ d)) →
    (∀ {c : C} (s s' : F.obj c ⟶ d),
        ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s') →
      CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
self_le_add_right : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [CanonicallyOrderedAdd α] (a b : α), a ≤ a + b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_alter!_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)} {fallback : α},
      (Std.DTreeMap.Internal.Impl.alter! k f t).isEmpty = false →
        ((Std.DTreeMap.Internal.Impl.alter! k f t).minKeyD fallback = k ↔
          (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true)
-- Mathlib.Combinatorics.Additive.Convolution
Finset.convolution.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  A.convolution B x = {ab ∈ A ×ˢ B | ab.1 * ab.2 = x}.card
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.preimage_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α} {t : Set β}, ContinuousWithinAt f s x → t ∈ nhds (f x) → f ⁻¹' t ∈ nhdsWithin x s
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem_toList_rcc : ∀ {m n : ℤ} {i : ℕ} (_h : i < (m...=n).toList.length), (m...=n).toList[i] = m + ↑i
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.symm : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x y : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F x y),
  CommRingCat.Colimits.Relation.below x_1 → motive x y x_1 → CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.left_adjoint_additive : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [G.Additive], F.Additive
-- Mathlib.Analysis.Complex.Trigonometric
/-- The real cotangent function, defined as the real part of the complex cotangent  -/
Real.cot : ℝ → ℝ
-- Init.Data.String.OrderInstances
String.Pos.instAntisymmLe : ∀ {s : String}, Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.WF → t.isEmpty = false → ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Lean.Meta.Tactic.NormCast
/-- The `push_cast` simp attribute.  -/
Lean.Meta.NormCast.pushCastExt : Lean.Meta.SimpExtension
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromTarget.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C}
  {Q : CategoryTheory.MorphismProperty C}, (∀ {X Y : C} (f : X ⟶ Y), Q f → P Y → P X) → P.InheritedFromTarget Q
-- Mathlib.FieldTheory.SeparableDegree
/-- The separable degree of any field extension `E / F` divides the degree of `E / F`.  -/
Field.finSepDegree_dvd_finrank : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.finSepDegree F E ∣ Module.finrank F E
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The natural isomorphism `mapTrifunctor F I₁ I₂ I₃ ≅ mapTrifunctor F' I₁ I₂ I₃`
induced by a natural isomorphism `F ≅ F'` of trifunctors.  -/
CategoryTheory.GradedObject.mapTrifunctorMapIso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                {F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))} →
                  (F ≅ F') →
                    (I₁ : Type u_7) →
                      (I₂ : Type u_8) →
                        (I₃ : Type u_9) →
                          CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃ ≅
                            CategoryTheory.GradedObject.mapTrifunctor F' I₁ I₂ I₃
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.add_neg_eq_add_neg_iff_of_isAddUnit : ∀ {M : Type u_1} [inst : SubtractionMonoid M] {a b c d : M},
  AddCommute b d → IsAddUnit b → IsAddUnit d → (a + -b = c + -d ↔ a + d = c + b)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, t.contains k = true → (cmp t.minKey! k).isLE = true
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.State.mk.injEq : ∀ (mctx : Lean.MetavarContext) (nextMacroScope : Lean.MacroScope) (ngen : Lean.NameGenerator)
  (cache : Std.HashMap Lean.ExprStructEq Lean.Expr) (mctx_1 : Lean.MetavarContext) (nextMacroScope_1 : Lean.MacroScope)
  (ngen_1 : Lean.NameGenerator) (cache_1 : Std.HashMap Lean.ExprStructEq Lean.Expr),
  ({ mctx := mctx, nextMacroScope := nextMacroScope, ngen := ngen, cache := cache } =
      { mctx := mctx_1, nextMacroScope := nextMacroScope_1, ngen := ngen_1, cache := cache_1 }) =
    (mctx = mctx_1 ∧ nextMacroScope = nextMacroScope_1 ∧ ngen = ngen_1 ∧ cache = cache_1)
-- Init.Data.String.Subslice
String.Slice.Subslice.startInclusive_cast : ∀ {s t : String.Slice} {h : s.copy = t.copy} {sl : s.Subslice},
  (String.Slice.Subslice.cast h sl).startInclusive = sl.startInclusive.cast h
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M` and a Localization map `f : M →+ N` away from `x`, we get an isomorphism between
the Localization of `M` at the Submonoid generated by `x` as a quotient type and `N`.  -/
AddLocalization.Away.addEquivOfQuotient : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {N : Type u_2} →
      [inst_1 : AddCommMonoid N] → (x : M) → AddSubmonoid.LocalizationMap.AwayMap x N → AddLocalization.Away x ≃+ N
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.exactAt_chainComplex_of_hasDimensionLT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [CategoryTheory.CategoryWithHomology C] (n d : ℕ)
  [X.HasDimensionLT d],
  autoParam (d ≤ n) SSet.exactAt_chainComplex_of_hasDimensionLT._auto_1 →
    HomologicalComplex.ExactAt (X.chainComplex R) n
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.primaryComponent_torsionBySet_eq_inf : ∀ {A : Type u_1} (M : Type u_2) [inst : CommRing A] [inst_1 : AddCommMonoid M] [inst_2 : Module A M] (I : Ideal A),
  Submodule.map (Submodule.torsionBySet A M ↑I).subtype (Ideal.primaryComponent (↥(Submodule.torsionBySet A M ↑I)) I) =
    Ideal.primaryComponent M I ⊓ Submodule.torsionBySet A M ↑I
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.single_mul : ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] (a : α) (b₁ b₂ : β),
  (fun₀ | a => b₁ * b₂) = (fun₀ | a => b₁) * fun₀ | a => b₂
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instIsMulCommutative_iSup : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} [Nonempty ι] [inst_2 : Preorder ι] [IsDirectedOrder ι]
  {S : ι →o Subgroup G} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₅_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  {φ φ' : f ⟶ g},
  φ = φ' ↔
    CategoryTheory.ComposableArrows.app' φ 0 _proof_449✝ = CategoryTheory.ComposableArrows.app' φ' 0 _proof_449✝ ∧
      CategoryTheory.ComposableArrows.app' φ 1 _proof_450✝ = CategoryTheory.ComposableArrows.app' φ' 1 _proof_450✝ ∧
        CategoryTheory.ComposableArrows.app' φ 2 _proof_451✝ = CategoryTheory.ComposableArrows.app' φ' 2 _proof_451✝ ∧
          CategoryTheory.ComposableArrows.app' φ 3 _proof_452✝ = CategoryTheory.ComposableArrows.app' φ' 3 _proof_452✝ ∧
            CategoryTheory.ComposableArrows.app' φ 4 _proof_453✝ =
                CategoryTheory.ComposableArrows.app' φ' 4 _proof_453✝ ∧
              CategoryTheory.ComposableArrows.app' φ 5 _proof_454✝ =
                CategoryTheory.ComposableArrows.app' φ' 5 _proof_454✝
-- Batteries.Data.PairingHeap
/-- `O(1)`. Returns the smallest element in the heap, or `none` if the heap is empty.  -/
Batteries.PairingHeap.head? : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le → Option α
-- Mathlib.Control.Monad.Writer
WriterT.instMonadOfMonoid : {M : Type u → Type v} → {ω : Type u} → [Monad M] → [Monoid ω] → Monad (WriterT ω M)
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorRightUnitor_hasMap : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] (p : J × I → J),
  (∀ (j : J), p (j, 0) = j) →
    ∀ (X : CategoryTheory.GradedObject J D),
      (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
            ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
        p
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [inst_2 : Inhabited β] {a : α} {c : ℕ},
  Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c) a = default
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_sub : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M) (a b : A),
  D (a - b) = D a - D b
-- Init.Data.List.Basic
List.lookup_nil : ∀ {α : Type u} {β : Type v} {a : α} [inst : BEq α], List.lookup a [] = none