mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Counters.mk : Lean.PHashMap Lean.Meta.Grind.Origin ℕ →
  Lean.PHashMap Lean.FVarId Lean.Name → Lean.PHashMap Lean.Name ℕ → Lean.PHashMap Lean.Name ℕ → Lean.Meta.Grind.Counters
-- Mathlib.Analysis.Convex.Independent
/-- **Alias** of `convexIndependent_set_iff_notMem_convexHull_sdiff`.

---

If a set is convex independent, a point in the set is not in the convex hull of the other
points. See `convexIndependent_iff_notMem_convexHull_sdiff` for the indexed family version.  -/
convexIndependent_set_iff_notMem_convexHull_diff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E}, ConvexIndependent 𝕜 Subtype.val ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Restriction of a semigroup hom to a subsemigroup of the codomain.  -/
MulHom.codRestrict : {M : Type u_1} →
  {N : Type u_2} →
    {σ : Type u_4} →
      [inst : Mul M] →
        [inst_1 : Mul N] →
          [inst_2 : SetLike σ N] →
            [inst_3 : MulMemClass σ N] → (f : M →ₙ* N) → (S : σ) → (∀ (x : M), f x ∈ S) → M →ₙ* ↥S
-- Lean.Widget.UserWidget
Lean.Widget.instToJsonUserWidgetDefinition.toJson : Lean.Widget.UserWidgetDefinition → Lean.Json
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.forget_δ : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Mon.forget C) X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.cast.congr_simp : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ g₀ g₁ : C(X, Y)}
  (F F_1 : f₀.Homotopy f₁), F = F_1 → ∀ (h₀ : f₀ = g₀) (h₁ : f₁ = g₁), F.cast h₀ h₁ = F_1.cast h₀ h₁
-- Mathlib.Algebra.DirectSum.Internal
/-- Build a `DirectSum.GCommSemiring` instance for a collection of additive submonoids.  -/
SetLike.gcommSemiring : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : AddCommMonoid ι] →
        [inst_1 : CommSemiring R] →
          [inst_2 : SetLike σ R] →
            [inst_3 : AddSubmonoidClass σ R] →
              (A : ι → σ) → [SetLike.GradedMonoid A] → DirectSum.GCommSemiring fun i => ↥(A i)
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.zpow_nonneg`

---

ZPowers of analytic functions (into a normed division algebra over `𝕜`) are analytic if the
exponent is nonnegative.  -/
AnalyticAt.fun_zpow_nonneg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {z : E} {n : ℤ}, AnalyticAt 𝕜 f z → 0 ≤ n → AnalyticAt 𝕜 (fun i => f i ^ n) z
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.range_lift : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A)
  (cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)),
  ((CliffordAlgebra.lift Q) ⟨f, cond⟩).range = Algebra.adjoin R (Set.range ⇑f)
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.lift_unique : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (f : X → L)
  (g : FreeLieAlgebra R X →ₗ⁅R⁆ L), ⇑g ∘ FreeLieAlgebra.of R = f ↔ g = (FreeLieAlgebra.lift R) f
-- Mathlib.Data.List.PeriodicityLemma
/-- If `w` has a period `p`, then any of its factors has a period `p` as well.  -/
List.HasPeriod.factor : ∀ {α : Type u_1} {u v w : List α} {p : ℕ}, (u ++ v ++ w).HasPeriod p → v.HasPeriod p
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ΨSq_ofNat : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℕ),
  W.ΨSq ↑n = W.preΨ' n ^ 2 * if Even n then W.Ψ₂Sq else 1
-- Mathlib.Data.Finset.Lattice.Basic
Finset.mem_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The seminorm is invariant under negation.  -/
AddGroupSeminorm.neg' : ∀ {G : Type u_6} [inst : AddGroup G] (self : AddGroupSeminorm G) (r : G), self.toFun (-r) = self.toFun r
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.restricted.eq_1 : ∀ (n : ℕ) (p : ℕ → Prop) [inst : DecidablePred p], Nat.Partition.restricted n p = {x | ∀ i ∈ x.parts, p i}
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.colimit F = (CategoryTheory.Limits.colimit.cocone F).pt
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The obvious factorisation of a monomorphism through itself.  -/
CategoryTheory.Limits.MonoFactorisation.self : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Mono f] → CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.head_val' : ∀ {α : Type u} {m : ℕ} {n' : Type uₙ} (B : Fin m.succ → n' → α) (j : n'),
  (Matrix.vecHead fun i => B i j) = Matrix.vecHead B j
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get!ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α]
  (l : Std.DTreeMap.Internal.Impl α β) (k : α) [inst_3 : Inhabited (β k)], l.get!ₘ k = (l.get?ₘ k).get!
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.forall_mem_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} {p : G → Prop},
  (∀ g ∈ AddSubgroup.zmultiples x, p g) ↔ ∀ (m : ℤ), p (m • x)
-- Init.Data.Option.Instances
Option.mem_def : ∀ {α : Type u_1} {a : α} {b : Option α}, a ∈ b ↔ b = some a
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.mkGlobalDiag : Lean.Meta.Grind.Counters →
  Lean.Meta.Simp.Stats → Lean.PArray Lean.Meta.Grind.SplitDiagInfo → Lean.MetaM (Option Lean.MessageData)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminormClass.toAddGroupSeminormClass : ∀ {E : Type u_3} {F : Type u_4} [inst : FunLike F E ℝ] [inst_1 : AddGroup E] [NonarchAddGroupSeminormClass F E],
  AddGroupSeminormClass F E ℝ
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffs_eq_empty_of_subsingleton : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Subsingleton R] (p : MvPolynomial σ R), p.coeffs = ∅
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The vector space of functions on `Fin n` has `finrank` equal to `n`.  -/
Module.finrank_fin_fun : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {n : ℕ}, Module.finrank R (Fin n → R) = n
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldlM.eq_2 : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_3} [inst : Monad m] (f : σ → α → m σ) (x : σ)
  (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  RBTree.RBNode.foldlM f x (RBTree.RBNode.node c l v r) = do
    let __do_lift ← RBTree.RBNode.foldlM f x l
    let __do_lift ← f __do_lift v
    RBTree.RBNode.foldlM f __do_lift r
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_add : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddZeroClass (f i)] (i : I) (x y : f i),
  Pi.single i (x + y) = Pi.single i x + Pi.single i y
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instOrderBot : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → [T1Space M] → OrderBot (ClosedSubmodule R M)
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqns.mk.inj : ∀ {eqnNames : Array Lean.Name} {splitterName : Lean.Name} {splitterMatchInfo : Lean.Meta.MatcherInfo}
  {eqnNames_1 : Array Lean.Name} {splitterName_1 : Lean.Name} {splitterMatchInfo_1 : Lean.Meta.MatcherInfo},
  { eqnNames := eqnNames, splitterName := splitterName, splitterMatchInfo := splitterMatchInfo } =
      { eqnNames := eqnNames_1, splitterName := splitterName_1, splitterMatchInfo := splitterMatchInfo_1 } →
    eqnNames = eqnNames_1 ∧ splitterName = splitterName_1 ∧ splitterMatchInfo = splitterMatchInfo_1
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.isValidForSlice : ∀ {pat s : String.Slice} {needlePos stackPos : String.Pos.Raw},
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos →
    String.Pos.Raw.IsValidForSlice s (stackPos.unoffsetBy needlePos)
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- Companion lemma to `MeromorphicOn.exists_ecanonicalDecomp`: In the setting of the extended canonical
decomposition, write the function `h` entirely in terms of `f`.
 -/
Complex.ECanonicalDecomp.eq_smul_meromorphicTrailingCoeffAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {w : ℂ} {f h : ℂ → E},
  Complex.ECanonicalDecomp f h R →
    w ∈ Metric.closedBall 0 R →
      0 < R →
        h w =
          ((∏ᶠ (i : ℂ),
                meromorphicTrailingCoeffAt (Complex.canonicalFactor R i) w ^
                  (MeromorphicOn.divisor f (Metric.ball 0 R)) i) *
              ∏ᶠ (i : ℂ),
                meromorphicTrailingCoeffAt (fun x => x - i) w ^ (-MeromorphicOn.divisor f (Metric.sphere 0 R)) i) •
            meromorphicTrailingCoeffAt f w
-- Std.Http.Data.URI.Encoding
/-- Proof that all characters in the byte array are valid encoded query characters.
 -/
Std.Http.URI.EncodedQueryString.valid : ∀ {r : UInt8 → Bool} (self : Std.Http.URI.EncodedQueryString r),
  Std.Http.URI.IsAllowedEncodedQueryChars r self.toByteArray
-- Aesop.Rule.Forward
Aesop.instInhabitedForwardRule : Inhabited Aesop.ForwardRule
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.op_obj_map : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D) (X : Dᵒᵖ) {X_1 Y : Cᵒᵖᵒᵖ} (f : X_1 ⟶ Y),
  (P.op.obj X).map f = (P.map f.unop.unop).app X
-- Init.Data.String.Basic
String.Slice.Pos.offset_ofStr : ∀ {s : String.Slice} {pos : s.str.Pos} {h₁ : s.startInclusive ≤ pos} {h₂ : pos ≤ s.endExclusive},
  (String.Slice.Pos.ofStr pos h₁ h₂).offset = pos.offset.unoffsetBy s.startInclusive.offset
-- Mathlib.Order.Hom.Lattice
SupHom.instFunLike.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β],
  SupHom.instFunLike = { coe := SupHom.toFun, coe_injective := ⋯ }
-- Lean.Parser.Extension
Lean.Parser.leadingIdentBehavior : Lean.Environment → Lean.Name → Lean.Parser.LeadingIdentBehavior
-- Std.Data.ExtTreeMap.Basic
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.ExtTreeMap.all : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → (α → β → Bool) → Bool
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_enumerateCountable_countableGeneratingSet : ∀ (α : Type u_3) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (n : ℕ),
  MeasurableSet (Set.enumerateCountable ⋯ ∅ n)
-- Mathlib.CategoryTheory.MarkovCategory.Positive
/-- Given morphisms `f : X ⟶ Y` and `g : Y ⟶ Z`, if their composition is deterministic, then
process `f`, copy and then process `g` equals copy and process `f` and `g` independently.  -/
CategoryTheory.PositiveCategory.copy_comp_natural : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.PositiveCategory C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [h : CategoryTheory.Deterministic (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
        (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id Y))) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) f)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.applyPartition_eq : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] [inst_1 : Std.TransOrd α] {k : α → Ordering}
  [inst_2 : Std.Internal.IsStrictCut compare k] {l : Std.DTreeMap.Internal.Impl α β}
  {f :
    List ((a : α) × β a) →
      (c : Std.DTreeMap.Internal.Cell α β k) →
        (Std.DTreeMap.Internal.Impl.contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ}
  (hlo : l.Ordered),
  Std.DTreeMap.Internal.Impl.applyPartition k l f =
    f (List.filter (fun x => k x.fst == Ordering.gt) l.toListModel)
      (Std.DTreeMap.Internal.List.findCell l.toListModel k) ⋯
      (List.filter (fun x => k x.fst == Ordering.lt) l.toListModel)
-- Mathlib.Topology.Constructions
CofiniteTopology.mem_nhds_iff : ∀ {X : Type u} {x : CofiniteTopology X} {s : Set (CofiniteTopology X)}, s ∈ nhds x ↔ x ∈ s ∧ sᶜ.Finite
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.gradedAddHom_apply_coe : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_4 : AddSubmonoidClass σ A]
  [inst_5 : AddSubmonoidClass τ B] (f : 𝒜 →+*ᵍ ℬ) (i : ι) (x : ↥(𝒜 i)), ↑((f.gradedAddHom i) x) = f ↑x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
Lean.Meta.Grind.Arith.CommRing.getCommSemiringId? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicInterior_subset : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, intrinsicInterior 𝕜 s ⊆ s
-- Qq.Match
Qq.Impl.PatternVar.mk.sizeOf_spec : ∀ (name : Lean.Name) (arity : ℕ) (mvar : Lean.Expr) (stx : Lean.Term),
  sizeOf { name := name, arity := arity, mvar := mvar, stx := stx } =
    1 + sizeOf name + sizeOf arity + sizeOf mvar + sizeOf stx
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- Builds the equivalence class of a Cauchy sequence of rationals.  -/
Padic.mk : {p : ℕ} → [inst : Fact (Nat.Prime p)] → PadicSeq p → ℚ_[p]
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.zipWith_neLocus_eq_left : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] {M : α → Type u_3} {P : α → Type u_4}
  [inst_1 : (a : α) → Zero (N a)] [inst_2 : (a : α) → Zero (M a)] [inst_3 : (a : α) → Zero (P a)]
  [inst_4 : (a : α) → DecidableEq (N a)] [inst_5 : (a : α) → DecidableEq (P a)] {F : (a : α) → M a → N a → P a}
  (F0 : ∀ (a : α), F a 0 0 = 0) (f : Π₀ (a : α), M a) (g₁ g₂ : Π₀ (a : α), N a),
  (∀ (a : α) (f : M a), Function.Injective fun g => F a f g) →
    (DFinsupp.zipWith F F0 f g₁).neLocus (DFinsupp.zipWith F F0 f g₂) = g₁.neLocus g₂
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedMap : (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsClosedMap).RespectsIso
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.coe_prod : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (s : AddSubmonoid M)
  (t : AddSubmonoid N), ↑(s.prod t) = ↑s ×ˢ ↑t
-- Mathlib.Order.RelSeries
/-- Given a series `a₀ -r→ a₁ -r→ ... -r→ aₙ` and an `a` such that `aₙ -r→ a` holds, there is
a series of length `n+1`: `a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ a`.
 -/
RelSeries.snoc : {α : Type u_1} → {r : SetRel α α} → (p : RelSeries r) → (newLast : α) → (p.last, newLast) ∈ r → RelSeries r
-- Mathlib.RingTheory.Jacobson.Radical
Ring.le_comap_jacobson : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Ring R] [inst_1 : Ring R₂] (f : R →+* R₂) [RingHomSurjective f],
  Ring.jacobson R ≤ Ideal.comap f (Ring.jacobson R₂)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrpObjIsoOfRepresentableBy.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  (F : CategoryTheory.Functor Cᵒᵖ AddGrpCat) (α : (F.comp (CategoryTheory.forget AddGrpCat)).RepresentableBy X),
  CategoryTheory.yonedaAddGrpObjIsoOfRepresentableBy X F α =
    CategoryTheory.NatIso.ofComponents
      (fun Y =>
        (let __Equiv := α.homEquiv;
          { toEquiv := __Equiv, map_add' := ⋯ }).toAddGrpIso)
      ⋯
-- Mathlib.Algebra.Colimit.Ring
/-- Noncomputable multiplicative inverse in a direct limit of fields.  -/
Field.DirectLimit.inv : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [Nonempty ι] →
        [IsDirectedOrder ι] →
          [inst_3 : (i : ι) → Field (G i)] →
            (f : (i j : ι) → i ≤ j → G i → G j) → Ring.DirectLimit G f → Ring.DirectLimit G f
-- Mathlib.Algebra.Order.Module.Defs
smul_max_of_nonpos : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : AddCommGroup β]
  [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β] {a : α},
  a ≤ 0 → ∀ (b₁ b₂ : β), a • max b₁ b₂ = min (a • b₁) (a • b₂)
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.absNorm_pow_inertiaDeg`. -/
Ideal.absNorm_pow_inertiaDeg' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [Module.Finite R S] [q.IsPrime] [q.LiesOver p] [inst_6 : IsDedekindDomain R]
  [inst_7 : IsDedekindDomain S] [inst_8 : Module.Free ℤ R] [inst_9 : Module.Free ℤ S],
  Ideal.absNorm p ^ q.inertiaDeg R = Ideal.absNorm q
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_sub_natCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ),
  ⌊a - ↑n⌋ = ⌊a⌋ - ↑n
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The induced map from the quotient by the kernel to the range.  -/
QuotientAddGroup.rangeKerLift : {G : Type u} → [inst : AddGroup G] → {H : Type v} → [inst_1 : AddGroup H] → (φ : G →+ H) → G ⧸ φ.ker →+ ↥φ.range
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.finYoneda_obj : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) (X : FintypeCatᵒᵖ),
  (LightCondensed.finYoneda F).obj X =
    ((Opposite.unop X).obj → F.obj (FintypeCat.toLightProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))
-- Init.Data.List.Lemmas
List.head_dropLast : ∀ {α : Type u_1} {xs : List α} (h : xs.dropLast ≠ []), xs.dropLast.head h = xs.head ⋯
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instIsScalarTower : ∀ {S : Type u_1} {T : Type u_2} {R : Type u_3} {c₁ c₂ c₃ : R} [inst : SMul S R] [inst_1 : SMul T R] [inst_2 : SMul S T]
  [IsScalarTower S T R], IsScalarTower S T (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.iSup_restrict_spanningSets : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SigmaFinite μ]
  (s : Set α), ⨆ i, (μ.restrict (MeasureTheory.spanningSets μ i)) s = μ s
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d.eq_5 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (a a_1 : ℕ),
  h.d (Int.negSucc a) (Int.ofNat a_1) =
    match Int.negSucc a, Int.ofNat a_1 with
    | Int.ofNat n, Int.ofNat m => L.d n m
    | Int.negSucc n, Int.negSucc m => K.d n m
    | Int.negSucc 0, Int.ofNat 0 => h.d₀
    | Int.ofNat a, Int.negSucc a_2 => 0
    | Int.negSucc a, Int.ofNat a_2 => 0
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
          Z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- If the R- and A-actions on M and N satisfy `CompatibleSMul` both ways,
then `M ⊗[A] N` is canonically isomorphic to `M ⊗[R] N` as `S`-modules,
where `S` is any other ring acting on `M` and whose action commutes with the `A` and `R`-actions.  -/
TensorProduct.equivOfCompatibleSMul : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_22) →
      (S : Type u_23) →
        (M : Type u_24) →
          (N : Type u_25) →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid N] →
                [inst_3 : Module R M] →
                  [inst_4 : Module R N] →
                    [inst_5 : CommSemiring A] →
                      [inst_6 : Module A M] →
                        [inst_7 : Module A N] →
                          [SMulCommClass R A M] →
                            [inst_9 : CommSemiring S] →
                              [inst_10 : Module S M] →
                                [inst_11 : SMulCommClass R S M] →
                                  [inst_12 : SMulCommClass A S M] →
                                    [TensorProduct.CompatibleSMul R A M N] →
                                      [TensorProduct.CompatibleSMul A R M N] →
                                        TensorProduct A M N ≃ₗ[S] TensorProduct R M N
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.Context.mk.sizeOf_spec : ∀ (proof : Lean.Expr) (xs : Array Lean.Expr), sizeOf { proof := proof, xs := xs } = 1 + sizeOf proof + sizeOf xs
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.isUnit_basicOpen_end : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : R),
  IsUnit
    ((algebraMap R
        (Module.End R ((AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))))
      f)
-- Mathlib.Geometry.Convex.Cone.Basic
/-- Galois insertion between `ConvexCone` and `SetLike.coe`.  -/
ConvexCone.gi : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → GaloisInsertion (ConvexCone.hull R) SetLike.coe
-- Init.Data.Nat.Gcd
_private.Init.Data.Nat.Gcd.0.Nat.gcd.eq_1 : ∀ (m n : ℕ), m.gcd n = if m = 0 then n else (n % m).gcd m
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAt.congr_simp : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (f f_1 : F → 𝕜),
  f = f_1 → ∀ (f' f'_1 : F), f' = f'_1 → ∀ (x x_1 : F), x = x_1 → HasGradientAt f f' x = HasGradientAt f_1 f'_1 x_1
-- Std.Do.WP.SimpLemmas
EStateM.orElse.eq_1 : ∀ {ε σ α δ : Type u} [inst : EStateM.Backtrackable δ σ] (x₁ : EStateM ε σ α) (x₂ : Unit → EStateM ε σ α) (s : σ),
  x₁.orElse x₂ s =
    match x₁ s with
    | EStateM.Result.error a s_1 => x₂ () (EStateM.Backtrackable.restore s_1 (EStateM.Backtrackable.save s))
    | ok => ok