mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_filter_containsKey_of_containsKey_eq_false_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getValueD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback =
        fallback
-- Mathlib.Order.SuccPred.Basic
/-- `PredOrder` transfers across equivalences between orders.  -/
PredOrder.ofOrderIso : {X : Type u_3} → {Y : Type u_4} → [inst : Preorder X] → [inst_1 : Preorder Y] → [PredOrder X] → X ≃o Y → PredOrder Y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanExt_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
  (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.one = iZ
-- Std.Async.Basic
/-- Runs an action, ensuring that some other action always happens afterward.
 -/
Std.Async.EAsync.tryFinally' : {ε α β : Type} →
  Std.Async.EAsync ε α →
    (Option α → Std.Async.EAsync ε β) →
      optParam Task.Priority Task.Priority.default → optParam Bool false → Std.Async.EAsync ε (α × β)
-- Mathlib.Algebra.Group.Subgroup.Even
/-- In a commutative additive monoid `M`, `AddSubmonoid.even M`
is the submonoid of even elements in `M`.  -/
AddSubmonoid.even : (M : Type u_1) → [inst : AddCommMonoid M] → AddSubmonoid M
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.boundary.eq_1 : ∀ {n : ℕ} (c : Composition n), c.boundary = OrderEmbedding.ofStrictMono (fun i => ⟨c.sizeUpTo ↑i, ⋯⟩) ⋯
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquiv_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {ι : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] [inst_6 : TopologicalSpace N] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N']
  [inst_9 : TopologicalSpace N'] (e : N ≃L[R] N'),
  ⇑e.continuousAlternatingMapCongrRightEquiv = (↑e).compContinuousAlternatingMap
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.measurable_cauchyPDF : ∀ (x₀ : ℝ) (γ : NNReal), Measurable (ProbabilityTheory.cauchyPDF x₀ γ)
-- Init.Data.Char.Basic
Char.isValidChar_zero : isValidChar 0
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_eq_of_mul_norm_lt_max : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] {x y : S}, ‖x * y‖ < max ‖x‖ ‖y‖ → ‖x‖ = ‖y‖
-- Init.Data.Nat.Lemmas
Nat.pow_le_pow_iff_right : ∀ {a n m : ℕ}, 1 < a → (a ^ n ≤ a ^ m ↔ n ≤ m)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.transEventuallyEqIsLittleO : {α : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : Norm E] →
        [inst_1 : Norm F] →
          {l : Filter α} → Trans (fun x1 x2 => x1 =ᶠ[l] x2) (fun x1 x2 => x1 =o[l] x2) fun x1 x2 => x1 =o[l] x2
-- Mathlib.Data.Fintype.Card
Finset.eq_univ_of_card : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s.card = Fintype.card α → s = Finset.univ
-- Mathlib.Order.Circular
CircularOrder.mk : {α : Type u_1} →
  [toCircularPartialOrder : CircularPartialOrder α] → (∀ (a b c : α), btw a b c ∨ btw c b a) → CircularOrder α
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  {G :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))}
  (φ : F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G)
  {P Q : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} (f : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom φ P)
      (F.op.whiskerLeft (G.map f)) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom φ Q)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) {X : D} (x : ℱ.obj (Opposite.op X)) (x_1 : D) (x_2 : x_1 ⟶ X)
  (hf : CategoryTheory.Presieve.coverByImage G X x_2),
  CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x x_2 hf =
    (CategoryTheory.ConcreteCategory.hom (ℱ'.obj.map (Nonempty.some hf).lift.op))
      ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op (Nonempty.some hf).1)))
        ((CategoryTheory.ConcreteCategory.hom (ℱ.map (Nonempty.some hf).map.op)) x))
-- Mathlib.Data.TypeVec
TypeVec.dropFun_subtypeVal : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)),
  TypeVec.dropFun (TypeVec.subtypeVal p) = TypeVec.subtypeVal (TypeVec.dropFun p)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isSome_get?_iff_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α},
  (Std.DTreeMap.Const.get? t a).isSome = true ↔ a ∈ t
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comap_sup : ∀ {X Y : AlgebraicGeometry.Scheme} (J₁ J₂ : Y.IdealSheafData) (f : X ⟶ Y), (J₁ ⊔ J₂).comap f = J₁.comap f ⊔ J₂.comap f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxView_k_eq_maxView! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced}
  {hr : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size},
  (Std.DTreeMap.Internal.Impl.maxView k v l r hl hr hlr).k = (Std.DTreeMap.Internal.Impl.maxView! k v l r).k
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the 201 status code.
 -/
Std.Http.Response.created : Std.Http.Response.Builder
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instCoeSortProfiniteAddGrpType : CoeSort ProfiniteAddGrp.{u} (Type u)
-- Init.Grind.Ordered.Order
Lean.Grind.LinearOrder.le_of_not_lt : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {a b : α}, ¬a < b → b ≤ a
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.symmetry.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full], hf'.symmetry hg = hf'.symmetry hg
-- Lean.AuxRecursor
Lean.mkRecOnName : Lean.Name → Lean.Name
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1 : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat}, (SheafOfModules.toSheaf R).ReflectsIsomorphisms
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalenceInlOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [(HomotopicalAlgebra.trivialCofibrations C).IsStableUnderCobaseChange]
  [HomotopicalAlgebra.Cofibration g] [HomotopicalAlgebra.WeakEquivalence g],
  HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.pushout.inl f g)
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
posTangentConeAt_univ : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : E}, posTangentConeAt Set.univ a = Set.univ
-- Init.Data.BitVec.Lemmas
BitVec.two_mul_toInt_le : ∀ {w : ℕ} {x : BitVec w}, 2 * x.toInt ≤ 2 ^ w - 1
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
/-- Nerves of finite non-empty ordinals are representable functors.  -/
CategoryTheory.nerve.representableBy : {n : ℕ} →
  (α : Type u) →
    [inst : Preorder α] →
      α ≃o Fin (n + 1) → CategoryTheory.Functor.RepresentableBy (CategoryTheory.nerve α) { len := n }
-- Mathlib.Data.Set.NAry
Set.subset_image2_sdiff_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β},
  Set.image2 f s t \ Set.image2 f s' t ⊆ Set.image2 f (s \ s') t
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSumRight.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₂ : Type v₂}
  [inst_3 : DecidableEq ι₂] (M₁' : Type w₁') (M₂ : ι₂ → Type w₂) [inst_4 : AddCommMonoid M₁']
  [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [inst_6 : Module R M₁'] [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_8 : Module S M₁'] [inst_9 : IsScalarTower R S M₁'],
  TensorProduct.directSumRight R S M₁' M₂ =
    TensorProduct.AlgebraTensorModule.congr (DirectSum.lid S M₁' PUnit.{1}).symm 1 ≪≫ₗ
        TensorProduct.directSum R S (fun x => M₁') M₂ ≪≫ₗ
      DirectSum.lequivCongrLeft S (Equiv.uniqueProd ι₂ Unit)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωSup_total : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {c : OmegaCompletePartialOrder.Chain α} {x : α},
  (∀ (i : ℕ), c i ≤ x ∨ x ≤ c i) → OmegaCompletePartialOrder.ωSup c ≤ x ∨ x ≤ OmegaCompletePartialOrder.ωSup c
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_filter_le_size : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool},
  t.WF → (Std.TreeSet.Raw.filter f t).size ≤ t.size
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.any_toList : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool}, it.toList.any p = Std.Iter.any p it
-- Mathlib.Data.DFinsupp.Defs
/-- Coercion from a `DFinsupp` to a pi type is an `AddMonoidHom`.  -/
DFinsupp.coeFnAddMonoidHom : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddZeroClass (β i)] → (Π₀ (i : ι), β i) →+ (i : ι) → β i
-- Lean.Environment
Lean.Kernel.Exception.typeExpected.injEq : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (expr : Lean.Expr) (env_1 : Lean.Kernel.Environment)
  (lctx_1 : Lean.LocalContext) (expr_1 : Lean.Expr),
  (Lean.Kernel.Exception.typeExpected env lctx expr = Lean.Kernel.Exception.typeExpected env_1 lctx_1 expr_1) =
    (env = env_1 ∧ lctx = lctx_1 ∧ expr = expr_1)
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.to_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤),
  HasStrictFDerivAt (HasStrictFDerivAt.implicitFunction f f' hf hf' (f a)) (↑f').ker.subtypeL 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertMany_nil : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.insertMany [] = t
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sMod.eq_1 : ∀ (p : ℕ), LucasLehmer.sMod p 0 = 4 % (2 ^ p - 1)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.eval_charpoly : ∀ {R : Type u_1} [inst : CommRing R] {m : Type u_3} [inst_1 : DecidableEq m] [inst_2 : Fintype m] (M : Matrix m m R)
  (t : R), Polynomial.eval t M.charpoly = ((Matrix.scalar m) t - M).det
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∪ t₂).getKey? k = t₂.getKey? k
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_loopyOn : ∀ {α : Type u_1} {β : Type u_2} {E : Set α} (f : α → β) (hf : Set.InjOn f (Matroid.loopyOn E).E),
  (Matroid.loopyOn E).map f hf = Matroid.loopyOn (f '' E)
-- Mathlib.Data.Finset.Card
Finset.exists_mem_notMem_of_card_lt_card : ∀ {α : Type u_1} {s t : Finset α}, s.card < t.card → ∃ e ∈ t, e ∉ s
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitForward_naturality₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A)
  (X Y : C) (f : X ⟶ Y)
  (p : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) Y),
  CategoryTheory.OverPresheafAux.unitForward η X
      (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) f
        p) =
    (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (CategoryTheory.OverPresheafAux.unitForward η Y p)
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_coe_finset : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : DecidableEq α] (s : Finset α),
  AddAction.stabilizer G ↑s = AddAction.stabilizer G s
-- Init.WF
/-- A type that has a standard well-founded relation.

Instances are used to prove that functions terminate using well-founded recursion by showing that
recursive calls reduce some measure according to a well-founded relation. This relation can combine
well-founded relations on the recursive function's parameters.
 -/
WellFoundedRelation : Sort u → Sort (max 1 u)
-- Init.Data.UInt.Lemmas
UInt64.zero_def : 0 = { toBitVec := 0 }
-- Mathlib.Topology.Order.LocalExtr
Filter.EventuallyLE.isLocalMinOn : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {f g : α → β} {a : α},
  f ≤ᶠ[nhdsWithin a s] g → f a = g a → IsLocalMinOn f s a → IsLocalMinOn g s a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.add_neg_of_nonpos_of_neg`.  -/
Left.add_neg_of_nonpos_of_neg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b : α},
  a ≤ 0 → b < 0 → a + b < 0
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `zero_apply`. -/
CuspForm.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The right adjoint to `left`.  -/
CategoryTheory.Bicategory.RightAdjoint.right : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} → {left : a ⟶ b} → CategoryTheory.Bicategory.RightAdjoint left → (b ⟶ a)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcOptions.mk.sizeOf_spec : ∀ (highlightMatchesProvider? : Option Lean.Lsp.HighlightMatchesOptions)
  (rpcWireFormat? : Option Lean.Lsp.RpcWireFormat),
  sizeOf { highlightMatchesProvider? := highlightMatchesProvider?, rpcWireFormat? := rpcWireFormat? } =
    1 + sizeOf highlightMatchesProvider? + sizeOf rpcWireFormat?
-- Mathlib.Tactic.FunProp.Theorems
/-- Function theorems are stated in uncurried or compositional form.

uncurried
```
theorem Continuous_add : Continuous (fun x ↦ x.1 + x.2)
```

compositional
```
theorem Continuous_add (hf : Continuous f) (hg : Continuous g) : Continuous (fun x ↦ (f x) + (g x))
```
 -/
Mathlib.Meta.FunProp.TheoremForm : Type
-- Mathlib.Data.Set.Image
Option.injective_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Option α → β},
  Function.Injective f ↔ Function.Injective (f ∘ some) ∧ f none ∉ Set.range (f ∘ some)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R],
  ⌈0⌉₊ = 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.transfer_self : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.transfer G ⋯ = p
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getZeroThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.Order.BoundedOrder.Basic
Prod.fst_bot : ∀ (α : Type u) (β : Type v) [inst : Bot α] [inst_1 : Bot β], ⊥.1 = ⊥
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The forgetful functor from bimodule objects to the ambient category.  -/
Bimod.forget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : CategoryTheory.Mon C) → {B : CategoryTheory.Mon C} → CategoryTheory.Functor (Bimod A B) C
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- The exponent of an element `a ∈ L` of a purely inseparable field extension `L / K`
is the smallest natural number `e` such that `a ^ ringExpChar K ^ e ∈ K`.  -/
IsPurelyInseparable.elemExponent : (K : Type u_2) →
  {L : Type u_3} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → [IsPurelyInseparable K L] → L → ℕ
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_self_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] (a : α) {b : α}, a / b ≤ a ↔ 1 ≤ b
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.mem_map_of_mem : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M} {r : M}, r ∈ p → f r ∈ Submodule.map f p
-- Lean.Meta.Basic
/-- Execute `x`. If it throws an error, indent and prepend `msg` to it.   -/
Lean.Meta.prependError : {m : Type → Type u_1} → {α : Type} → [MonadControlT Lean.MetaM m] → [Monad m] → Lean.MessageData → m α → m α
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piFinTwo_symm_apply : ∀ (α : Fin 2 → Type u) [inst : (i : Fin 2) → UniformSpace (α i)],
  ⇑(UniformEquiv.piFinTwo α).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.toLinearMap_toPerfPair : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [inst_5 : p.IsPerfPair] (x : M),
  p.toPerfPair x = p x
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instMul.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S],
  OreLocalization.instMul = { mul := OreLocalization.smul }
-- Mathlib.Data.List.Destutter
/-- `destutter` of relations like `≠`, whose negation is an equivalence relation,
gives a list of maximal length over any chain.

In other words, `l.destutter R` is an `R`-chain sublist of `l`, and is at least as long as any other
`R`-chain sublist.  -/
List.IsChain.length_le_length_destutter : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] [IsEquiv α Rᶜ] {l₁ l₂ : List α},
  l₁.Sublist l₂ → List.IsChain R l₁ → l₁.length ≤ (List.destutter R l₂).length
-- Mathlib.RingTheory.LocalProperties.Semilocal
/-- A submodule `N` of a module `M` over a semilocal ring `R` is finitely generated if
its localization at every maximal ideal is finitely generated.  -/
Submodule.fg_of_isLocalized_maximal : ∀ {R : Type u_1} [inst : CommSemiring R] [Finite (MaximalSpectrum R)] {M : Type u_2} [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3)
  [inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)]
  [inst_5 : (P : Ideal R) → [inst_5 : P.IsMaximal] → Algebra R (Rₚ P)]
  [inst_6 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4) [inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst_8 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)]
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
  (f : (P : Ideal R) → [inst_11 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_11 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M),
  (∀ (P : Ideal R) [inst_12 : P.IsMaximal], (Submodule.localized' (Rₚ P) P.primeCompl (f P) N).FG) → N.FG
-- Mathlib.Data.WSeq.Defs
/-- Get the index of the first occurrence of `a` in `s`  -/
Stream'.WSeq.indexOf : {α : Type u} → [DecidableEq α] → α → Stream'.WSeq α → Computation ℕ
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (a : α), MeasurableSet {a}
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.neg_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b : α),
  -Set.uIcc a b = Set.uIcc (-a) (-b)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.bot_quotient_isMaximal_iff : ∀ {R : Type u} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided], ⊥.IsMaximal ↔ I.IsMaximal
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- If
* `p : ι' → MvPolynomial ι K` is a family of polynomials (which in practice will be homogeneous
  of the same degree `N`),
* `q : ι × ι' → MvPolynomial ι K` is a family of homogeneous polynomials of the same degree `M`,
* `x : ι → K` is such that for all `k : ι`,
  `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,

then the logarithmic height of `fun j ↦ (p j).eval x` is bounded below by an (explicit)
constant depending only on `q` plus `N` times the logarithmic height of `x`.  -/
Height.logHeight_eval_ge : ∀ {K : Type u_6} [inst : Field K] {ι : Type u_7} {ι' : Type u_8} [inst_1 : Fintype ι']
  [inst_2 : Height.AdmissibleAbsValues K] [Finite ι] {M N : ℕ} {q : ι × ι' → MvPolynomial ι K},
  (∀ (a : ι × ι'), (q a).IsHomogeneous M) →
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K},
      (∀ (k : ι), ∑ j, (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (p j) = x k ^ (M + N)) →
        -Real.log (↑(Nat.card ι') ^ Height.totalWeight K * max (Height.mulHeightBound q) 1) + ↑N * Height.logHeight x ≤
          Height.logHeight fun j => (MvPolynomial.eval x) (p j)
-- Mathlib.Data.FinEnum
FinEnum.PSigma.finEnumPropLeft : {α : Prop} → {β : α → Type v} → [(a : α) → FinEnum (β a)] → [Decidable α] → FinEnum ((a : α) ×' β a)
-- Mathlib.FieldTheory.SeparableClosure
Field.instNeZeroFinInsepDegree : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E],
  NeZero (Field.finInsepDegree F E)
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a.fmod b
-- Mathlib.Algebra.Group.Basic
pow_sub_one_mul : ∀ {M : Type u_4} [inst : Monoid M] {n : ℕ}, n ≠ 0 → ∀ (a : M), a ^ (n - 1) * a = a ^ n
-- Mathlib.RingTheory.Extension.ExtendScalars
/-- Given an extension `P` of `S` over `R`, `P.extendScalars` is the same extension
but viewed as an extension of `S` over `P.Ring`.  -/
Algebra.Extension.extendScalars : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → Algebra.Extension P.Ring S