mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformlyOn.hasProd : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {x : β} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasProdLocallyUniformlyOn f g s → x ∈ s → HasProd (fun x_1 => f x_1 x) (g x)
-- Mathlib.Data.Multiset.FinsetOps
Multiset.length_ndinsert_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∉ s → (Multiset.ndinsert a s).card = s.card + 1
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.instHasHomology : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c')
  [∀ (j : ι), K.HasHomology j] (j' : ι'), (K.extend e).HasHomology j'
-- Mathlib.Topology.NhdsWithin
nhdsWithin_basis_open : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (t : Set α),
  (nhdsWithin a t).HasBasis (fun u => a ∈ u ∧ IsOpen u) fun u => u ∩ t
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.eq_append_of_dropPrefix?_prop_eq_some : ∀ {P : Char → Prop} [inst : DecidablePred P] {s res : String.Slice},
  s.dropPrefix? P = some res → ∃ c, s.copy = String.singleton c ++ res.copy ∧ P c
-- Mathlib.Tactic.FunProp.ToBatteries
/-- Beta reduces head of an expression, `(fun x => e) a` ==> `e[x/a]`. This version applies
arguments through let bindings without inlining them.

Example
```
headBeta' ((fun x => let y := x * x; fun z => x + y + z) a b)
==>
let y := a * a; a + y + b
```
 -/
Mathlib.Meta.FunProp.headBetaThroughLet : Lean.Expr → Lean.Expr
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toContinuousAddMonoidHom_comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂),
  ↑(h ∘SL f) = (↑h).comp ↑f
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.instMonoFL₀'OfL₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) [CategoryTheory.Mono S.L₁.f], CategoryTheory.Mono S.L₀'.f
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.relabel.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α → β) (l : ℕ) (_f : L.Functions l)
  (ts : Fin l → L.Term α),
  FirstOrder.Language.Term.relabel g (FirstOrder.Language.func _f ts) =
    FirstOrder.Language.func _f fun {i} => FirstOrder.Language.Term.relabel g (ts i)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₁_comp : ∀ {X Y : SSet} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp SSet.ι₁
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (SSet.stdSimplex.obj { len := 1 })) =
    CategoryTheory.CategoryStruct.comp f SSet.ι₁
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.tensorEquiv.eq_1 : ∀ (R : Type u_1) {M : Type u_2} {N : Type u_3} [inst : CommSemiring R],
  AddMonoidAlgebra.tensorEquiv R =
    ((TensorProduct.congr (AddMonoidAlgebra.coeffLinearEquiv R) (AddMonoidAlgebra.coeffLinearEquiv R)).trans
          (finsuppTensorFinsupp' R M N)).trans
      (AddMonoidAlgebra.coeffLinearEquiv R).symm
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- A morphism version of `le_sup_right`.  -/
CategoryTheory.MonoOver.leSupRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasImages C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] →
        {A : C} → (f g : CategoryTheory.MonoOver A) → g ⟶ (CategoryTheory.MonoOver.sup.obj f).obj g
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t ≠ ∅}, (cmp k (t.minKey he)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.isomorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (J : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} J],
  (CategoryTheory.MorphismProperty.isomorphisms C).IsStableUnderColimitsOfShape J
-- Mathlib.Probability.Independence.Integration
/-- The scalar product of two independent and integrable random variables is integrable.  -/
ProbabilityTheory.IndepFun.integrable_smul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6}
  [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] [inst_2 : MeasurableSpace E] [OpensMeasurableSpace E]
  [inst_4 : TopologicalSpace F] [inst_5 : ContinuousENorm F] [inst_6 : MeasurableSpace F] [OpensMeasurableSpace F]
  [inst_8 : SMul E F] [ContinuousSMul E F] [ENormSMulClass E F] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.Integrable X μ → MeasureTheory.Integrable Y μ → MeasureTheory.Integrable (fun ω => X ω • Y ω) μ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool}, (Std.DHashMap.filter f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), f k (m.get k h) = true
-- Mathlib.Data.Finset.Lattice.Fold
/-- To rewrite from right to left, use `Finset.inf'_comp_eq_map`.  -/
Finset.inf'_map : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] {s : Finset γ} {f : γ ↪ β} (g : β → α)
  (hs : (Finset.map f s).Nonempty), (Finset.map f s).inf' hs g = s.inf' ⋯ (g ∘ ⇑f)
-- Lean.Meta.LitValues
/-- Return `some ⟨n, v⟩` if `e` is:
- an `OfNat.ofNat` application
- a `BitVec.ofNat` application
- a `BitVec.ofNatLT` application
that encode a `BitVec n` with value `v`.
 -/
Lean.Meta.getBitVecValue? : Lean.Expr → Lean.MetaM (Option ((n : ℕ) × BitVec n))
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_eq_expSeries_rat : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] [inst_5 : Algebra ℚ 𝔸] (n : ℕ),
  ⇑(NormedSpace.expSeries 𝕂 𝔸 n) = ⇑(NormedSpace.expSeries ℚ 𝔸 n)
-- Mathlib.MeasureTheory.Measure.Support
/-- Under the assumption `OpensMeasurableSpace`, this is redundant because
the complement of the support is open, and therefore measurable.  -/
MeasureTheory.Measure.nullMeasurableSet_compl_support : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [HereditarilyLindelofSpace X], MeasureTheory.NullMeasurableSet μ.supportᶜ μ
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Sum of a multiset of elements in a `Subring` of a `Ring` is
in the `Subring`.  -/
Subring.multiset_sum_mem : ∀ {R : Type u_1} [inst : Ring R] (s : Subring R) (m : Multiset R), (∀ a ∈ m, a ∈ s) → m.sum ∈ s
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_inj : ∀ {a b : BitVec 32}, Int32.ofBitVec a = Int32.ofBitVec b ↔ a = b
-- Mathlib.Logic.Basic
imp_congr_ctx_eq : ∀ {a b c d : Prop}, a = c → (c → b = d) → (a → b) = (c → d)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instGroup : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → Group (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] → Group (DirectLimit G f)
-- Mathlib.Topology.Category.LightProfinite.Basic
instFullFintypeCatLightProfiniteToLightProfinite : FintypeCat.toLightProfinite.Full
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Functor.associator_inv_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' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  (H : CategoryTheory.Functor E E') (x : C),
  (F.associator G H).inv.app x = CategoryTheory.CategoryStruct.id ((F.comp (G.comp H)).obj x)
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_single_of_ne : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (a : Γ) {r : R},
  r ≠ 0 → ((HahnSeries.single a) r).cardSupp = 1
-- Plausible.Shrinkable
/-- `Nat.shrink' n` creates a list of smaller natural numbers by
successively dividing `n` by 2 . For example, `Nat.shrink 5 = [2, 1, 0]`.  -/
Plausible.Nat.shrink : ℕ → List ℕ
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
ContinuousLinearMap.mk.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_3}
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommMonoid M] {M₂ : Type u_4} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂] (toLinearMap toLinearMap_1 : M →ₛₗ[σ] M₂)
  (e_toLinearMap : toLinearMap = toLinearMap_1) (cont : Continuous toLinearMap.toFun),
  { toLinearMap := toLinearMap, cont := cont } = { toLinearMap := toLinearMap_1, cont := ⋯ }
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
_private.Mathlib.NumberTheory.LSeries.DirichletContinuation.0.DirichletCharacter.LFunction_changeLevel_aux : ∀ {M N : ℕ} [inst : NeZero M] [inst_1 : NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ},
  s ≠ 1 →
    DirichletCharacter.LFunction ((DirichletCharacter.changeLevel hMN) χ) s =
      DirichletCharacter.LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_le_mul_of_nonneg_of_nonpos : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R]
  [AddRightMono R] [AddRightReflectLE R], c ≤ a → b ≤ d → 0 ≤ c → b ≤ 0 → a * b ≤ c * d
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr_bisim : ∀ {α : Type u_1} {β : Type u_2} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {xs : List.Vector α n} {f₁ : α → σ₁ → σ₁ × β}
  {f₂ : α → σ₂ → σ₂ × β} {s₁ : σ₁} {s₂ : σ₂} (R : σ₁ → σ₂ → Prop),
  R s₁ s₂ →
    (∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2) →
      R (List.Vector.mapAccumr f₁ xs s₁).1 (List.Vector.mapAccumr f₂ xs s₂).1 ∧
        (List.Vector.mapAccumr f₁ xs s₁).2 = (List.Vector.mapAccumr f₂ xs s₂).2
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.sub_def : ∀ {K : Type u_1} [inst : CommRing K] (x x_1 : RatFunc K),
  x.sub x_1 =
    match x, x_1 with
    | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p - q }
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.mem_matrix : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocRing R] [inst_1 : Fintype n] (I : TwoSidedIdeal R)
  (M : Matrix n n R), M ∈ TwoSidedIdeal.matrix n I ↔ ∀ (i j : n), M i j ∈ I
-- Init.Grind.Module.Basic
Lean.Grind.IntModule.toAddCommGroup : {M : Type u} → [self : Lean.Grind.IntModule M] → Lean.Grind.AddCommGroup M
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (h : F.CoreMonoidal) (X Y : C),
  CategoryTheory.Functor.LaxMonoidal.μ F X Y = (h.μIso X Y).hom
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.liftRingHom_symm_apply_coe : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R] (F : (DirectSum ι fun i => A i) →+* R)
  {i : ι}, ↑(DirectSum.liftRingHom.symm F) = (↑F).comp (DirectSum.of A i)
-- Init.Data.Vector.Lemmas
Vector.getElem?_of_mem : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n}, a ∈ xs → ∃ i, xs[i]? = some a
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_fun_const_smul : ∀ {𝕜 : 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} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [inst_7 : SMulCommClass 𝕜 R F]
  [inst_8 : ContinuousConstSMul R F],
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 f s x → ∀ (c : R), fderivWithin 𝕜 (fun y => c • f y) s x = c • fderivWithin 𝕜 f s x
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- The isomorphism `(K.extend e).X i' ≅ K.X i` when `e.f i = i'`.  -/
HomologicalComplex.extendXIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
              [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                (K : HomologicalComplex C c) →
                  (e : c.Embedding c') → {i' : ι'} → {i : ι} → e.f i = i' → ((K.extend e).X i' ≅ K.X i)
-- Lean.Data.PersistentArray
Lean.PersistentArray.modify : {α : Type u} → [Inhabited α] → Lean.PersistentArray α → ℕ → (α → α) → Lean.PersistentArray α
-- Init.Data.Option.Lemmas
Option.rel_none_none : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, Option.Rel r none none
-- Init.Data.String.Lemmas.FindPos
String.Slice.le_offset_posGE : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p ≤ s.rawEndPos}, p ≤ (s.posGE p h).offset
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If we have `IsCofiltered C`, then for any functor `F : J ⥤ C` with `FinCategory J`,
there exists a cone over `F`.
 -/
CategoryTheory.IsCofiltered.cone_nonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] {J : Type w}
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C),
  Nonempty (CategoryTheory.Limits.Cone F)
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If a function `f` tends to infinity along a filter,
then `f` multiplied by a negative constant (on the left) tends to negative infinity.  -/
Filter.Tendsto.const_mul_atTop_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => r * f x) l Filter.atBot
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_le_zpow_iff_right_of_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {m n : ℤ}, 0 < a → a < 1 → (a ^ m ≤ a ^ n ↔ n ≤ m)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- The equivalence relation indicating that two points are in the same cycle of a permutation.  -/
Equiv.Perm.SameCycle : {α : Type u_2} → Equiv.Perm α → α → α → Prop
-- Mathlib.Order.SymmDiff
bihimp_left_comm : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b c : α), bihimp a (bihimp b c) = bihimp b (bihimp a c)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instSub : {α : Type u_5} → [inst : NonUnitalNonAssocRing α] → Sub (CentroidHom α)
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Nonempty.ciSup_lt_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set ι} {a : α} {f : ι → α},
  s.Nonempty → s.Finite → (⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a)
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.add_apply : ∀ {M : Type u_8} {N : Type u_9} [inst : Zero M] [inst_1 : AddZeroClass N] (f g : ZeroHom M N) (x : M),
  (f + g) x = f x + g x
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- The finite separable degree multiply by the finite inseparable degree is equal
to the (finite) field extension degree.  -/
Field.finSepDegree_mul_finInsepDegree : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.finSepDegree F E * Field.finInsepDegree F E = Module.finrank F E
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The identity morphism on a module object.  -/
CategoryTheory.Mod.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.MonObj A] → (M : CategoryTheory.Mod D A) → M.Hom M
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x x' : C} (f : x ⟶ x') (y : C) (z : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x'
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj y z) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj y z))
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x y z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f y) z)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x' y z).hom h))
-- Lean.Parser.Basic
Lean.Parser.sepBy : Lean.Parser.Parser →
  (sep : String) → optParam Lean.Parser.Parser (Lean.Parser.symbol sep) → optParam Bool false → Lean.Parser.Parser
-- Lean.Elab.DefView
/-- Short name. Recall that all declarations in Lean 4 are potentially recursive. We use `shortDeclName` to refer
to them at `valueStx`, and other declarations in the same mutual block.  -/
Lean.Elab.DefViewElabHeaderData.shortDeclName : Lean.Elab.DefViewElabHeaderData → Lean.Name
-- Init.Data.Range.Basic
Membership.mem.lower : ∀ {i : ℕ} {r : Std.Legacy.Range}, i ∈ r → r.start ≤ i
-- Init.Data.String.Lemmas.Slice
String.Slice.front?_eq_get? : ∀ {s : String.Slice}, s.front? = s.startPos.get?
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_add_subset : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p q : MvPolynomial σ R),
  (p + q).vars ⊆ p.vars ∪ q.vars
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac._auto_1)
  [inst_2 : CategoryTheory.Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
  [inst_3 : CategoryTheory.Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.map' k (k + 1) ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp (hS.cokerToKer k hk)
        (CategoryTheory.Limits.kernel.ι (S.map' (k + 2) (k + 3) ⋯ ⋯))) =
    S.map' (k + 1) (k + 2) ⋯ ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- The isomorphism `toHoCat ⋙ toLocalization L ≅ ι ⋙ L` which expresses that
if `L : C ⥤ D` is a localization functor, then its restriction on the
full subcategory of fibrant objects factors through the homotopy category
of fibrant objects.  -/
HomotopicalAlgebra.FibrantObject.HoCat.toHoCatCompToLocalizationIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (L : CategoryTheory.Functor C D) →
            [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] →
              HomotopicalAlgebra.FibrantObject.toHoCat.comp (HomotopicalAlgebra.FibrantObject.HoCat.toLocalization L) ≅
                HomotopicalAlgebra.FibrantObject.ι.comp L
-- Mathlib.Logic.IsEmpty.Basic
leftTotal_iff_isEmpty_left : ∀ {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β], Relator.LeftTotal R ↔ IsEmpty α
-- Init.Data.Nat.Gcd
Nat.gcd_add_mul_left_left : ∀ (m n k : ℕ), (n + m * k).gcd m = n.gcd m
-- Init.Grind.Interactive
/-- Show `grind` state.  -/
Lean.Parser.Tactic.Grind.showState : Lean.ParserDescr
-- Mathlib.Algebra.Category.Grp.Ulift
GrpCat.instCreatesLimitsOfSizeUliftFunctor.eq_1 : GrpCat.instCreatesLimitsOfSizeUliftFunctor =
  {
    CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, u} J] =>
      { CreatesLimit := fun {x} => CategoryTheory.createsLimitOfFullyFaithfulOfPreserves } }
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- If `v` is `R`-linearly independent and `x` is not in the `K`-span of `range v` (where `K` is a
division ring extending `R` and acting on the same module), then `Fin.snoc v x` is `R`-linearly
independent.

This is useful when proving `ℤ`-linear independence using the fact that an element is outside the
`ℝ`-span, which arises naturally in lattice theory and geometry of numbers.  -/
LinearIndependent.finSnoc_of_not_mem_span_over : ∀ {R : Type u_6} {K : Type u_7} {M : Type u_8} [inst : CommRing R] [inst_1 : DivisionRing K] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R K] [inst_4 : Module K M] [inst_5 : Module R M] [IsScalarTower R K M] [FaithfulSMul R K] {n : ℕ}
  {v : Fin n → M},
  LinearIndependent R v → ∀ {x : M}, x ∉ Submodule.span K (Set.range v) → LinearIndependent R (Fin.snoc v x)
-- Std.Do.SPred.DerivedLaws
/-- Tautology in `SPred` as a quotable definition.  -/
Std.Do.SPred.Tactic.tautological : {σs : List (Type u)} → Std.Do.SPred σs → Prop
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, (t.insertMany l).contains k = (t.contains k || l.contains k)
-- Mathlib.Order.Filter.Bases.Basic
Filter.eventually_prod_self_iff : ∀ {α : Type u_1} {la : Filter α} {r : α → α → Prop},
  (∀ᶠ (x : α × α) in la ×ˢ la, r x.1 x.2) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).getKey k h' = m₁.getKey k ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insert : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {fallback v : β},
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl a fallback =
    if compare k a = Ordering.eq then v else Std.DTreeMap.Internal.Impl.Const.getD t a fallback
-- Mathlib.CategoryTheory.Core
CategoryTheory.coreCategory_id_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.Core C),
  (CategoryTheory.CategoryStruct.id X).iso = CategoryTheory.Iso.refl X.of