mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.toAlgHom_toIntAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R ≃+* S), ↑f.toIntAlgEquiv = (↑f).toIntAlgHom
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.insertEntry.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.insertEntry k v l =
    bif Std.Internal.List.containsKey k l then Std.Internal.List.replaceEntry k v l else ⟨k, v⟩ :: l
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F)
  (γ : Path a b), ∫ᶜ (x : E) in γ.symm, ω x = -∫ᶜ (x : E) in γ, ω x
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R}
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂),
  ((Matrix.toLinearMap₂' R) M).SeparatingRight ↔ ((Matrix.toLinearMap₂ b₁ b₂) M).SeparatingRight
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instCommMagmaQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : CommMagma R] → (c : RingCon R) → CommMagma c.Quotient
-- Mathlib.Topology.Algebra.AsymptoticCone
smul_mem_asymptoticCone_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set P} {c : k} {v : V},
  0 < c → (c • v ∈ asymptoticCone k s ↔ v ∈ asymptoticCone k s)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.eval_not : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVUnOp.not.eval = fun x => ~~~x
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.autMapHom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {A B : C}
  [inst_2 : CategoryTheory.PreGaloisCategory.IsConnected A] [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois B]
  (f : A ⟶ B) (σ : CategoryTheory.Aut A),
  (CategoryTheory.PreGaloisCategory.autMapHom f) σ = CategoryTheory.PreGaloisCategory.autMap f σ
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.unitCoeff_spec : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0), x = ↑(PadicInt.unitCoeff hx) * ↑p ^ x.valuation
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.subset_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I n M],
  atlas H M ⊆ IsManifold.maximalAtlas I n M
-- Mathlib.Data.List.Defs
/-- `consecutivePairs [a, b, c, d]` is `[(a, b), (b, c), (c, d)]`.  -/
List.consecutivePairs : {α : Type u_1} → List α → List (α × α)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.mem_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → (k ∈ m₁ ↔ k ∈ m₂)
-- Mathlib.Order.Lattice
ULift.instLinearOrder : {α : Type u} → [LinearOrder α] → LinearOrder (ULift.{v, u} α)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.forget₂Mon_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} (f : A ⟶ B), ((CategoryTheory.Grp.forget₂Mon C).map f).hom = f.hom.hom
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
pos_of_right_mul_lt_le : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b c : R} [ExistsAddOfLE R] [PosMulMono R]
  [AddRightMono R] [AddRightReflectLE R], a * b < a * c → b ≤ c → 0 < a
-- Mathlib.Data.Set.Function
Set.BijOn.union : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.BijOn f s₁ t₁ → Set.BijOn f s₂ t₂ → Set.InjOn f (s₁ ∪ s₂) → Set.BijOn f (s₁ ∪ s₂) (t₁ ∪ t₂)
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.lowerCentralSeries_eq_lcs_comap : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ) (N : LieSubmodule R L M)
  [LieModule R L M], LieModule.lowerCentralSeries R L (↥N) k = LieSubmodule.comap N.incl (LieSubmodule.lcs k N)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isSome_skipPrefix? : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.LawfulForwardPattern pat]
  {s : String.Slice}, (s.skipPrefix? pat).isSome = s.startsWith pat
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.ofRepr.inj : ∀ {ι : Type u_1} {G : Type u_2} {inst : AddGroup G} {repr repr_1 : G ≃+ FreeAddGroup ι},
  { repr := repr } = { repr := repr_1 } → repr = repr_1
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₂ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.ShortComplex.π₂
-- Init.Data.List.Lemmas
List.getElem_of_append : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {i : ℕ} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i),
  l[i] = a
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- A family of elements spanning the unit ideal of `R` gives an affine open cover of `Spec R`.  -/
AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop : {R : CommRingCat} →
  {ι : Type u_1} → (s : ι → ↑R) → Ideal.span (Set.range s) = ⊤ → (AlgebraicGeometry.Spec R).AffineOpenCover
-- Mathlib.Data.Matrix.Mul
Matrix.diagonal_mulVec_single : ∀ {n : Type u_3} {R : Type u_7} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : NonUnitalNonAssocSemiring R]
  (v : n → R) (j : n) (x : R), (Matrix.diagonal v).mulVec (Pi.single j x) = Pi.single j (v j * x)
-- Batteries.Data.PairingHeap
/-- `O(n log n)`. Convert the heap to an array in increasing order.  -/
Batteries.PairingHeapImp.Heap.toArray : {α : Type u_1} → (α → α → Bool) → Batteries.PairingHeapImp.Heap α → Array α
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.edgeMk_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : C),
  CategoryTheory.nerve.edgeMk (CategoryTheory.CategoryStruct.id x) = SSet.Edge.id (CategoryTheory.nerveEquiv.symm x)
-- Lean.DocString.Types
Lean.Doc.instBEqListItem.beq : {α : Type u_1} → [BEq α] → Lean.Doc.ListItem α → Lean.Doc.ListItem α → Bool
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Iic_add_one_comm : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : LinearOrder α] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : Add α] [inst_4 : One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M),
  ∏ i ≤ a + 1, f i = f (a + 1) * ∏ i ≤ a, f i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_maxKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey?.isSome = true ↔ t.isEmpty = false
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.preCDF_le_one : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ],
  ∀ᵐ (a : α) ∂ρ.fst, ∀ (r : ℚ), ProbabilityTheory.preCDF ρ r a ≤ 1
-- Mathlib.Util.AtLocation
/-- Throw an error if this action has no effect.  -/
Mathlib.Tactic.BehaviorIfUnchanged.error : Mathlib.Tactic.BehaviorIfUnchanged
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- **Alias** of `Metric.Snowflaking.preimage_toSnowflaking_eball`. -/
Metric.Snowflaking.preimage_toSnowflaking_emetricBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  (d : ENNReal),
  ⇑Metric.Snowflaking.toSnowflaking ⁻¹' Metric.eball x d = Metric.eball (Metric.Snowflaking.ofSnowflaking x) (d ^ α⁻¹)
-- Mathlib.Data.Finset.Max
Finset.min_union : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α}, (s ∪ t).min = min s.min t.min
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.collectUsed : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → optParam Lean.FVarIdHashSet ∅ → Lean.FVarIdHashSet
-- Std.Http.Data.URI.Encoding
/-- Decodes an `EncodedString` back to a regular `String`. Converts percent-encoded sequences (e.g., "%20")
back to their original characters. Returns `none` if the decoded bytes are not valid UTF-8.
 -/
Std.Http.URI.EncodedString.decode : {r : UInt8 → Bool} → Std.Http.URI.EncodedString r → Option String
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.instSetLikeSigmaHom : {C : Type u} → [inst : CategoryTheory.Groupoid C] → SetLike (CategoryTheory.Subgroupoid C) ((c : C) × (d : C) × (c ⟶ d))
-- Lean.Util.Recognizers
Lean.Expr.isDIte : Lean.Expr → Bool
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- In a pseudometric space, the extended distance is always finite  -/
edist_lt_top : ∀ {α : Type u_3} [inst : PseudoMetricSpace α] (x y : α), edist x y < ⊤
-- Init.Data.Option.Lemmas
Option.pfilter_eq_some_iff : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} {a : α},
  o.pfilter p = some a ↔ ∃ (ha : o = some a), p a ha = true
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter.eq_1 : ∀ {n : ℕ} (i₁ i₂ a : Fin (n + 1)),
  Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂
      (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a) =
    if a = i₁ ∨ a = i₂ then 1 else 0
-- Lean.Meta.Sym.DSimp.DSimpM
/-- No change. If `done = true`, skip remaining simplification steps for this term.  -/
Lean.Meta.Sym.DSimp.Result.rfl : optParam Bool false → Lean.Meta.Sym.DSimp.Result
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- If `S` is a faithfully flat `R`-algebra, then any faithfully flat `S`-Module is faithfully flat
as an `R`-module.  -/
Module.FaithfullyFlat.trans : ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M]
  [Module.FaithfullyFlat R S] [Module.FaithfullyFlat S M], Module.FaithfullyFlat R M
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.restrictFreeVar.match_1.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u_3} {β : Type u_5} [inst : DecidableEq α]
  (motive : (x : ℕ) → (x_1 : L.BoundedFormula α x) → (↥x_1.freeVarFinset → β) → Sort u_4) (_n : ℕ)
  (φ : L.BoundedFormula α (_n + 1)) (f : ↥φ.all.freeVarFinset → β)
  (h_1 :
    (_n : ℕ) →
      (_f : ↥FirstOrder.Language.BoundedFormula.falsum.freeVarFinset → β) →
        motive _n FirstOrder.Language.BoundedFormula.falsum _f)
  (h_2 :
    (_n : ℕ) →
      (t₁ t₂ : L.Term (α ⊕ Fin _n)) →
        (f : ↥(FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset → β) →
          motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂) f)
  (h_3 :
    (_n l : ℕ) →
      (R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin _n)) →
          (f : ↥(FirstOrder.Language.BoundedFormula.rel R ts).freeVarFinset → β) →
            motive _n (FirstOrder.Language.BoundedFormula.rel R ts) f)
  (h_4 : (_n : ℕ) → (φ₁ φ₂ : L.BoundedFormula α _n) → (f : ↥(φ₁.imp φ₂).freeVarFinset → β) → motive _n (φ₁.imp φ₂) f)
  (h_5 : (_n : ℕ) → (φ : L.BoundedFormula α (_n + 1)) → (f : ↥φ.all.freeVarFinset → β) → motive _n φ.all f),
  (match _n, φ.all, f with
    | _n, FirstOrder.Language.BoundedFormula.falsum, _f => h_1 _n _f
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂, f => h_2 _n t₁ t₂ f
    | _n, FirstOrder.Language.BoundedFormula.rel R ts, f => h_3 _n l R ts f
    | _n, φ₁.imp φ₂, f => h_4 _n φ₁ φ₂ f
    | _n, φ.all, f => h_5 _n φ f) =
    h_5 _n φ f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mk.inj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {inst_2 : CategoryTheory.Category.{v₃, u₃} C₃}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} {pt : C₂} {fst : pt ⟶ (G.obj (Opposite.op X₁)).obj X₃} {snd : pt ⟶ (G.obj (Opposite.op Y₁)).obj Y₃}
  {isPullback : CategoryTheory.IsPullback fst snd ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)}
  {π : (G.obj (Opposite.op Y₁)).obj X₃ ⟶ pt}
  {π_fst :
    autoParam (CategoryTheory.CategoryStruct.comp π fst = (G.map f₁.op).app X₃)
      CategoryTheory.Functor.PullbackObjObj.π_fst._autoParam}
  {π_snd :
    autoParam (CategoryTheory.CategoryStruct.comp π snd = (G.obj (Opposite.op Y₁)).map f₃)
      CategoryTheory.Functor.PullbackObjObj.π_snd._autoParam}
  {pt_1 : C₂} {fst_1 : pt_1 ⟶ (G.obj (Opposite.op X₁)).obj X₃} {snd_1 : pt_1 ⟶ (G.obj (Opposite.op Y₁)).obj Y₃}
  {isPullback_1 : CategoryTheory.IsPullback fst_1 snd_1 ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)}
  {π_1 : (G.obj (Opposite.op Y₁)).obj X₃ ⟶ pt_1}
  {π_fst_1 :
    autoParam (CategoryTheory.CategoryStruct.comp π_1 fst_1 = (G.map f₁.op).app X₃)
      CategoryTheory.Functor.PullbackObjObj.π_fst._autoParam}
  {π_snd_1 :
    autoParam (CategoryTheory.CategoryStruct.comp π_1 snd_1 = (G.obj (Opposite.op Y₁)).map f₃)
      CategoryTheory.Functor.PullbackObjObj.π_snd._autoParam},
  { pt := pt, fst := fst, snd := snd, isPullback := isPullback, π := π, π_fst := π_fst, π_snd := π_snd } =
      { pt := pt_1, fst := fst_1, snd := snd_1, isPullback := isPullback_1, π := π_1, π_fst := π_fst_1,
        π_snd := π_snd_1 } →
    pt = pt_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1 ∧ π ≍ π_1
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mem_closedBallAddSubgroup_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M}
  {c : ArchimedeanClass M}, a ∈ c.closedBallAddSubgroup ↔ c ≤ ArchimedeanClass.mk a
-- Mathlib.Algebra.Group.Hom.Instances
/-- If `G` is an additive commutative group, then so is `ZeroHom M G`.  -/
ZeroHom.instAddCommGroup : {M : Type uM} → {N : Type uN} → [inst : Zero M] → [inst_1 : AddCommGroup N] → AddCommGroup (ZeroHom M N)
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.coe_bot : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁}, ↑⊥ = ∅
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An `OrderAddMonoidHom` can be lifted to an `OrderHom` over archimedean classes.  -/
ArchimedeanClass.orderHom : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        {N : Type u_2} →
          [inst_3 : AddCommGroup N] →
            [inst_4 : LinearOrder N] →
              [inst_5 : IsOrderedAddMonoid N] → (M →+o N) → ArchimedeanClass M →o ArchimedeanClass N
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The left-inverse of `ι`.

As an implementation detail, we implement this using `TrivSqZeroExt` which has a suitable
algebra structure.  -/
ExteriorAlgebra.ιInv : {R : Type u1} →
  [inst : CommRing R] → {M : Type u2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → ExteriorAlgebra R M →ₗ[R] M
-- Mathlib.Data.Set.Functor
Set.instLawfulMonad : LawfulMonad Set
-- Std.Data.TreeSet.Basic
Std.TreeSet.instInsert : {α : Type u} → {cmp : α → α → Ordering} → Insert α (Std.TreeSet α cmp)
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.inferMVarType : Lean.MVarId → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Normed.Group.Defs
ENormedCommMonoid.toESeminormedCommMonoid : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ENormedCommMonoid E] → ESeminormedCommMonoid E
-- Mathlib.Algebra.Algebra.TransferInstance
/-- Transfer `Algebra` across an `Equiv`  -/
Equiv.algebra : (R : Type u_1) →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : CommSemiring R] →
        (e : α ≃ β) →
          [inst_1 : Semiring β] →
            have x := e.semiring;
            [Algebra R β] → Algebra R α
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_toSubmonoid : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G), ↑K.toSubmonoid = ↑K
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_cast_mul : ∀ {n : ℕ} (x y : ZMod n), (x * y).cast = x.cast * y.cast % ↑n
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_sublist_of_dvd : ∀ {n k : ℕ}, n ∣ k → k ≠ 0 → n.primeFactorsList.Sublist k.primeFactorsList
-- Init.Data.Vector.Lemmas
Vector.append_assoc_symm : ∀ {α : Type u_1} {n m k : ℕ} {xs : Vector α n} {ys : Vector α m} {zs : Vector α k},
  xs ++ (ys ++ zs) = Vector.cast ⋯ (xs ++ ys ++ zs)
-- Mathlib.Order.CountableSupClosed
countableInfClosure_singleton : ∀ {α : Type u_2} [inst : PartialOrder α] {x : α}, countableInfClosure {x} = {x}
-- Mathlib.Tactic.FunProp.Mor
/-- Given `f a₁ a₂ ... aₙ`, returns `#[a₁, ..., aₙ]` where `f` can be bundled morphism.  -/
Mathlib.Meta.FunProp.Mor.getAppArgs : Lean.Expr → Lean.MetaM (Array Mathlib.Meta.FunProp.Mor.Arg)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A linearly-ordered additive abelian group is cyclic iff it is isomorphic to `ℤ` as an ordered
additive monoid.  -/
LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int : ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A],
  IsAddCyclic A ↔ Nonempty (A ≃+o ℤ)
-- Init.Data.List.Monadic
List.anyM_pure : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → Bool} {as : List α},
  List.anyM (fun x => pure (p x)) as = pure (as.any p)
-- Mathlib.Data.Set.Function
Set.InjOn.ne_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {x y : α}, Set.InjOn f s → x ∈ s → y ∈ s → (f x ≠ f y ↔ x ≠ y)
-- Init.Data.Option.List
Option.forIn_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (o : Option α) (b : β)
  (f : α → β → m (ForInStep β)), forIn o.toList b f = forIn o b f
-- Mathlib.Order.LiminfLimsup
Filter.le_limsup_of_frequently_le' : ∀ {α : Type u_6} {β : Type u_7} [inst : CompleteLattice β] {f : Filter α} {u : α → β} {x : β},
  (∃ᶠ (a : α) in f, x ≤ u a) → x ≤ Filter.limsup u f
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.instEuclideanDomain : {R : Type u} → [inst : Field R] → EuclideanDomain (Polynomial R)
-- Mathlib.Algebra.Ring.Shrink
Shrink.instNonUnitalCommRing : {α : Type u_1} → [inst : Small.{v, u_1} α] → [NonUnitalCommRing α] → NonUnitalCommRing (Shrink.{v, u_1} α)
-- Mathlib.Data.Fintype.Pi
RelHom.instFintype : {α : Type u_3} →
  {β : Type u_4} →
    [Fintype α] →
      [Fintype β] →
        [DecidableEq α] →
          {r : α → α → Prop} → {s : β → β → Prop} → [DecidableRel r] → [DecidableRel s] → Fintype (r →r s)
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorUnivLevelPos.majorType.injEq : ∀ (idx idx_1 : ℕ),
  (Lean.Meta.RecursorUnivLevelPos.majorType idx = Lean.Meta.RecursorUnivLevelPos.majorType idx_1) = (idx = idx_1)
-- Lean.Elab.MutualInductive
/-- Like `finalize`, but occurs before `afterTypeChecking` attributes.  -/
Lean.Elab.Command.InductiveElabStep2.prefinalize : Lean.Elab.Command.InductiveElabStep2 →
  List Lean.Name →
    Array Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep3
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.containsThenInsert_snd : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.containsThenInsert k v).2 = t.insert k v
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofNat_of_lt : ∀ {n : ℕ}, n < UInt32.size → UInt32.toNat (OfNat.ofNat n) = n
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.reassign.inj : ∀ {xs : Array Lean.Elab.Term.Do.Var} {doElem : Lean.Syntax} {k : Lean.Elab.Term.Do.Code}
  {xs_1 : Array Lean.Elab.Term.Do.Var} {doElem_1 : Lean.Syntax} {k_1 : Lean.Elab.Term.Do.Code},
  Lean.Elab.Term.Do.Code.reassign xs doElem k = Lean.Elab.Term.Do.Code.reassign xs_1 doElem_1 k_1 →
    xs = xs_1 ∧ doElem = doElem_1 ∧ k = k_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.lt.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} (a : α) (a_1 : k a = Ordering.lt) (a_2 : β a)
  (a_3 : List ((a : α) × β a)) (a_4 : α) (a_5 : k a_4 = Ordering.lt) (a_6 : β a_4) (a_7 : List ((a : α) × β a)),
  (Std.DTreeMap.Internal.Impl.ExplorationStep.lt a a_1 a_2 a_3 =
      Std.DTreeMap.Internal.Impl.ExplorationStep.lt a_4 a_5 a_6 a_7) =
    (a = a_4 ∧ a_2 ≍ a_6 ∧ a_3 = a_7)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_symm_eq_iff_map_eq : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {N : Type u_5} [inst_1 : Group N] {H : Subgroup N} {e : G ≃* N},
  Subgroup.map (↑e.symm) H = K ↔ Subgroup.map (↑e) K = H
-- Mathlib.Algebra.Order.Group.Defs
IsOrderedAddMonoid.toIsOrderedCancelAddMonoid : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α], IsOrderedCancelAddMonoid α
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedContext : Inhabited Lean.Meta.Simp.Context
-- Mathlib.Data.Fintype.EquivFin
Fintype.one_lt_card_iff_nontrivial : ∀ {α : Type u_1} [inst : Fintype α], 1 < Fintype.card α ↔ Nontrivial α
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.partition.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (f : (a : α) → β a → Bool) (t : Std.DTreeMap.Raw α β cmp),
  Std.DTreeMap.Raw.partition f t =
    Std.DTreeMap.Raw.foldl
      (fun x a b =>
        match x with
        | (l, r) => if f a b = true then (l.insert a b, r) else (l, r.insert a b))
      (∅, ∅) t
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidt_ne_zero_coe : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] {f : ι → E}
  (n : ι), LinearIndependent 𝕜 (f ∘ Subtype.val) → InnerProductSpace.gramSchmidt 𝕜 f n ≠ 0
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimit_iff_of_noMax : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α],
  Order.IsSuccPrelimit a ↔ IsMin a
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The circumcenter of a simplex, in terms of `pointsWithCircumcenter`.  -/
Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
  s.circumcenter =
    (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter)
      (Affine.Simplex.circumcenterWeightsWithCircumcenter n)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_neg : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [inst_6 : TopologicalSpace A]
  [inst_7 : NonUnitalRing A] [inst_8 : StarRing A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [inst_12 : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  cfcₙ (fun x => -f x) a = -cfcₙ f a
-- Mathlib.Data.Set.Lattice
Set.notMem_of_notMem_sUnion : ∀ {α : Type u_1} {x : α} {t : Set α} {S : Set (Set α)}, x ∉ ⋃₀ S → t ∈ S → x ∉ t
-- Init.Data.UInt.Bitwise
USize.and_le_left : ∀ {a b : USize}, a &&& b ≤ a