mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of two `C^n` functions at a point is `C^n` at this point.  -/
ContDiffAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {n : WithTop ℕ∞} {𝕜' : Type u_3} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → ContDiffAt 𝕜 n (f • g) x
-- Mathlib.GroupTheory.Coset.Basic
leftCoset_eq_iff : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {x y : α}, x • ↑s = y • ↑s ↔ x⁻¹ * y ∈ s
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k k' : α},
      cmp k k' = Ordering.eq →
        k ∉ t →
          List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKey? k' = some k
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concatRecAux.eq_def : ∀ {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort u_1}
  (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil)
  (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)) {u v : V}
  (x : G.Walk u v),
  SimpleGraph.Walk.concatRecAux Hnil Hconcat x =
    match v, x with
    | .(u), SimpleGraph.Walk.nil => Hnil
    | v, SimpleGraph.Walk.cons h p => ⋯ ▸ Hconcat p.reverse ⋯ (SimpleGraph.Walk.concatRecAux Hnil Hconcat p)
-- Batteries.Data.Nat.Lemmas
Nat.recDiagAux_zero_right : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_left : (n : ℕ) → motive 0 n) (zero_right : (m : ℕ) → motive m 0)
  (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1)) (m : ℕ),
  autoParam (zero_left 0 = zero_right 0) Nat.recDiagAux_zero_right._auto_1 →
    Nat.recDiagAux zero_left zero_right succ_succ m 0 = zero_right m
-- Mathlib.Data.Finset.Insert
Finset.Nonempty.exists_eq_singleton_or_nontrivial : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → (∃ a, s = {a}) ∨ s.Nontrivial
-- Mathlib.Order.Filter.Cocardinal
Filter.instCardinalInterFilter_cocardinal : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular}, CardinalInterFilter (Filter.cocardinal α hreg) c
-- Mathlib.GroupTheory.OrderOfElement
Pi.orderOf : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → Monoid (α i)] [inst_1 : Fintype ι] (x : (i : ι) → α i),
  orderOf x = Finset.univ.lcm fun i => orderOf (x i)
-- Mathlib.Data.Multiset.Count
Multiset.count_injective : ∀ {α : Type u_1} [inst : DecidableEq α], Function.Injective fun s a => Multiset.count a s
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.eq_1 : ∀ (α : Type u_6), FreeMonoid α = List α
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsUniversal.below.of_isQF : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsUniversal → Prop} {n : ℕ}
  {φ : L.BoundedFormula α n} (h : φ.IsQF), FirstOrder.Language.BoundedFormula.IsUniversal.below ⋯
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.monotone_spanningSets : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ],
  Monotone (MeasureTheory.spanningSets μ)
-- Mathlib.Algebra.Category.Ring.Basic
/-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`.

An example where this is needed is in applying
`PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective`.
 -/
RingCat.forget_obj_eq_coe : RingCat → RingCat → Prop
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.distortion_biUnionPrepartition : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Fintype ι] (π : BoxIntegral.TaggedPrepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J),
  (π.biUnionPrepartition πi).distortion = π.boxes.sup fun J => (πi J).distortion
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.kroneckerStarAlgEquiv_symm_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] [inst_5 : StarRing R] (x : Matrix (m × n) (m × n) R),
  (Matrix.kroneckerStarAlgEquiv m n R).symm x = (kroneckerLinearEquiv m m n n R).symm x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If the product comparison morphism is an iso, its inverse is natural in the right argument.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerLeft_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B B' : C}
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)] (g : B ⟶ B')
  [inst_5 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B')] {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B') ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B')) h)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mul_mem_sup : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S T : StarSubalgebra R A} {x y : A},
  x ∈ S → y ∈ T → x * y ∈ S ⊔ T
-- Mathlib.Analysis.Convex.Between
wbtw_vsub_const_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (p : P), Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Wbtw R x y z
-- Mathlib.Topology.Order.OrderClosed
frontier_Ici_subset : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] (a : α),
  frontier (Set.Ici a) ⊆ {a}
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The `Equiv` between `index K` and `K →+* ℂ` defined by sending a real infinite place `w` to
the unique corresponding embedding `w.embedding`, and the pair `⟨w, 0⟩` (resp. `⟨w, 1⟩`) for a
complex infinite place `w` to `w.embedding` (resp. `conjugate w.embedding`).  -/
NumberField.mixedEmbedding.indexEquiv : (K : Type u_1) → [inst : Field K] → [NumberField K] → NumberField.mixedEmbedding.index K ≃ (K →+* ℂ)
-- Init.Data.Array.Lemmas
Array.mem_of_ne_of_mem : ∀ {α : Type u_1} {a y : α} {xs : Array α}, a ≠ y → a ∈ xs.push y → a ∈ xs
-- Mathlib.Algebra.Order.Module.Pointwise
BddAbove.smul_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [PosSMulMono α β] {a : α} {s : Set β}, BddAbove s → 0 ≤ a → BddAbove (a • s)
-- Mathlib.Logic.Equiv.Basic
Function.update_apply_equiv_apply : ∀ {α : Sort u_1} {β : Sort u_4} {α' : Sort u_9} [inst : DecidableEq α'] [inst_1 : DecidableEq α] (f : α → β)
  (g : α' ≃ α) (a : α) (v : β) (a' : α'), Function.update f a v (g a') = Function.update (f ∘ ⇑g) (g.symm a) v a'
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).minKey? = t.minKey?
-- Init.Guard
/-- Tactic to check that a named hypothesis has a given type and/or value.

* `guard_hyp h : t` checks the type up to reducible defeq,
* `guard_hyp h :~ t` checks the type up to default defeq,
* `guard_hyp h :ₛ t` checks the type up to syntactic equality,
* `guard_hyp h :ₐ t` checks the type up to alpha equality.
* `guard_hyp h := v` checks value up to reducible defeq,
* `guard_hyp h :=~ v` checks value up to default defeq,
* `guard_hyp h :=ₛ v` checks value up to syntactic equality,
* `guard_hyp h :=ₐ v` checks the value up to alpha equality.

The value `v` is elaborated using the type of `h` as the expected type.
 -/
Lean.Parser.Tactic.guardHypConv : Lean.ParserDescr
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isInt_lt_true : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [Nontrivial α] {a b : α} {a' b' : ℤ},
  Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' < b') = true → a < b
-- Lean.Elab.Do.Legacy
/-- Extending code blocks with variable declarations: `let x : t := v` and `let x : t ← v`.
We remove `x` from the collection of updated variables.
Remark: `stx` is the syntax for the declaration (e.g., `letDecl`), and `xs` are the variables
declared by it. It is an array because we have let-declarations that declare multiple variables.
Example: `let (x, y) := t`
 -/
Lean.Elab.Term.Do.mkVarDeclCore : Array Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Elab.Term.Do.CodeBlock → Lean.Elab.Term.Do.CodeBlock
-- Std.Http.Protocol.H1.Message
Std.Http.Protocol.H1.instReprHead : {dir : Std.Http.Protocol.H1.Direction} → Repr (Std.Http.Protocol.H1.Message.Head dir)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- If two 0-cells have the same characteristic image point, they are equal.  -/
Topology.RelCWComplex.injective_map_zero : ∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [inst : Topology.RelCWComplex C D],
  Function.Injective fun x => ↑(Topology.RelCWComplex.map 0 x) ![]
-- Mathlib.SetTheory.Ordinal.Basic
/-- **Alias** of `Ordinal.nonempty_toType_iff`. -/
Ordinal.toType_nonempty_iff_ne_zero : ∀ {o : Ordinal.{u_1}}, Nonempty o.ToType ↔ o ≠ 0
-- Mathlib.Topology.Order.OrderClosed
/-- A topology on a set which is both a topological space and a preorder is _order-closed_ if the
set of points `(x, y)` with `x ≤ y` is closed in the product space. We introduce this as a mixin.
This property is satisfied for the order topology on a linear order, but it can be satisfied more
generally, and suffices to derive many interesting properties relating order and topology.  -/
OrderClosedTopology : (α : Type u_1) → [TopologicalSpace α] → [Preorder α] → Prop
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.instForInOfMonad : {m : Type u_1 → Type u_2} → {α : Type u_3} → {cmp : α → α → Ordering} → [Monad m] → ForIn m (RBTree.RBSet α cmp) α
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.smul_coe : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (g : ↥(Subgroup.normalizer ↑H)) (h : ↥H),
  ↑(SMul.smul g h) = ↑g * ↑h * ↑g⁻¹
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.toList_eq_nil_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp],
  Std.ExtDTreeMap.Const.toList t = [] ↔ t = ∅
-- Lean.Class
/-- Type class environment extension
 -/
Lean.classExtension : Lean.SimplePersistentEnvExtension Lean.ClassEntry Lean.ClassState
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.inter_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ : Std.DTreeMap.Raw α β cmp}, t₁.WF → t₂.WF → t₃.WF → t₁.Equiv t₂ → (t₁ ∩ t₃).Equiv (t₂ ∩ t₃)
-- Mathlib.Order.Bounded
Set.unbounded_lt_of_unbounded_le : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  Set.Unbounded (fun x1 x2 => x1 ≤ x2) s → Set.Unbounded (fun x1 x2 => x1 < x2) s
-- Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Polynomial.IsDistinguishedAt.mul : ∀ {R : Type u_1} [inst : CommRing R] {f f' : Polynomial R} {I : Ideal R},
  f.IsDistinguishedAt I → f'.IsDistinguishedAt I → (f * f').IsDistinguishedAt I
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- Lift a `RingEquiv` to `WithAbs`.  -/
WithAbs.congr : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] →
      [inst_1 : PartialOrder S] →
        [inst_2 : Semiring R] →
          (v : AbsoluteValue R S) →
            {T : Type u_3} → [inst_3 : Semiring T] → (w : AbsoluteValue T S) → R ≃+* T → WithAbs v ≃+* WithAbs w
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.numBound_zero : ∀ (k : ℕ) (D : ℕ → ℕ), ChevalleyThm.MvPolynomialC.numBound k D 0 = k
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A metavariable. This key matches with anything. It stores an identifier.  -/
Lean.Meta.RefinedDiscrTree.Key.labelledStar : ℕ → Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Topology.Sheaves.Module
/-- Sheaves of modules over `R.over U` are equivalent to sheaves of modules over `R |_ U`.  -/
TopologicalSpace.Opens.sheafOfModulesEquivOver : {X : TopCat} →
  (U : TopologicalSpace.Opens ↑X) →
    (R : TopCat.Sheaf RingCat X) →
      SheafOfModules (CategoryTheory.Sheaf.over R U) ≌ SheafOfModules (U.sheafRestrict.obj R)
-- Mathlib.Order.Minimal
maximal_ge_iff : ∀ {α : Type u_2} {x y : α} [inst : Preorder α], Maximal (fun x => y ≤ x) x ↔ y ≤ x ∧ IsMax x
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.mk_eq_mk_iff_smul_eq_smul : ∀ {M : Type u_1} [inst : AddCommMonoid M] [IsAddTorsionFree M] {m m' : M} {s s' : ℕ+},
  DivisibleHull.mk m s = DivisibleHull.mk m' s' ↔ ↑s' • m = ↑s • m'
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- A predicate saying that in case `l.bRiemann = true`, the function `r` is a constant.  -/
BoxIntegral.IntegrationParams.RCond : {ι : Type u_2} → BoxIntegral.IntegrationParams → ((ι → ℝ) → ↑(Set.Ioi 0)) → Prop
-- Mathlib.RingTheory.Noetherian.Orzech
IsNoetherian.equivPUnitOfProdInjective_symm_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsNoetherian R M] (f : M × N →ₗ[R] M)
  (i : Function.Injective ⇑f) (x : PUnit.{w + 1}), (IsNoetherian.equivPUnitOfProdInjective f i).symm x = 0
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Right.inv_lt_self : ∀ {α : Type u} [inst : Group α] [inst_1 : Preorder α] [MulRightStrictMono α] {a : α}, 1 < a → a⁻¹ < a
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_self : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M), e.det ⇑e = 1
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β},
  s • t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.comp_injective_right : ∀ {V : Type u} [inst : Quiver V] {a b c : V} (p : Quiver.Path a b), Function.Injective p.comp
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ}, (Std.ExtHashMap.map f m).size = m.size
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the left unitor `λ_ f`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.leftUnitorM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Mathlib.Algebra.Algebra.Hom
AlgHom.ext_iff : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {φ₁ φ₂ : A →ₐ[R] B}, φ₁ = φ₂ ↔ ∀ (x : A), φ₁ x = φ₂ x
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_ofSubtype : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {p : α → Prop} [inst_2 : DecidablePred p]
  [inst_3 : Fintype (Subtype p)] {g : Equiv.Perm (Subtype p)}, (Equiv.Perm.ofSubtype g).cycleType = g.cycleType
-- Init.Omega.LinearCombo
Lean.Omega.instDecidableEqLinearCombo : DecidableEq Lean.Omega.LinearCombo
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Embedding of an affine subspace to the ambient space, as an affine map.  -/
AffineSubspace.subtype : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] →
            [inst_3 : AddTorsor V P] → (s : AffineSubspace k P) → [inst_4 : Nonempty ↥s] → ↥s →ᵃ[k] P
-- Mathlib.Data.Set.Image
Set.nonempty_preimage_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set β} {f : α → β}, (f ⁻¹' s).Nonempty ↔ (s ∩ Set.range f).Nonempty
-- Mathlib.Order.Partition.Basic
Partition.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : α} [inst_1 : SizeOf α] (parts : Set α) (sSupIndep' : sSupIndep parts)
  (bot_notMem' : ⊥ ∉ parts) (sSup_eq' : sSup parts = s),
  sizeOf { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' } =
    1 + sizeOf sSup_eq'
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_injective_iff : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  {a₁ a₂ : HomogeneousLocalization 𝒜 x}, a₁ = a₂ ↔ a₁.val = a₂.val
-- Mathlib.Data.Setoid.Partition
IndexedPartition.eq : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (i : ι), s i = {x | hs.index x = i}
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- A closed subspace of a proper space is proper.
This is true for any proper lipschitz map. See `LipschitzWith.properSpace`.  -/
ProperSpace.of_isClosed : ∀ {X : Type u_3} [inst : PseudoMetricSpace X] [ProperSpace X] {s : Set X}, IsClosed s → ProperSpace ↑s
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.inl_add_inr_eq_mk : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (m : α) (n : β), (OrderAddMonoidHom.inl α β) m + (OrderAddMonoidHom.inr α β) n = (m, n)
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.tdiv.match_1.eq_4 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.negSucc n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_4 m n
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDF_pos : ∀ (μ : ℝ) {v : NNReal}, v ≠ 0 → ∀ (x : ℝ), 0 < ProbabilityTheory.gaussianPDF μ v x
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The `Subgroup` generated by a set.  -/
Subgroup.closure : {G : Type u_1} → [inst : Group G] → Set G → Subgroup G
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq : ∀ {R : Type u_4} [inst : CommRing R] {V : Type u_5} [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V] {ι : Type u_6} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (b : Module.Basis ι R V) (g : ↥(Subgroup.center (Matrix.SpecialLinearGroup ι R))),
  ↑(((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)).trans SpecialLinearGroup.centerEquivRootsOfUnity)
        g) =
    ↑(Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity g)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instLE : {Ω : Type u_1} → {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → LE (MeasureTheory.Filtration ι m)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.ite.sizeOf_spec : ∀ (ref : Lean.Syntax) (h? : Option Lean.Elab.Term.Do.Var) (optIdent cond : Lean.Syntax)
  (thenBranch elseBranch : Lean.Elab.Term.Do.Code),
  sizeOf (Lean.Elab.Term.Do.Code.ite ref h? optIdent cond thenBranch elseBranch) =
    1 + sizeOf ref + sizeOf h? + sizeOf optIdent + sizeOf cond + sizeOf thenBranch + sizeOf elseBranch
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.labellingCostarEquiv_apply : ∀ {V : Type u_1} {M : Type u_2} [inst : Group M] [inst_1 : MulAction M V] {S : Type u_3} (ι : S → M)
  (x : Quiver.SchreierGraph V ι) (a : Quiver.Costar x),
  (Quiver.SchreierGraph.labellingCostarEquiv ι x) a = (Quiver.SchreierGraph.labelling V ι).costar x a
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_pow : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {i : σ} {f : MvPolynomial σ R} {n : ℕ},
  (MvPolynomial.pderiv i) (f ^ n) = ↑n * f ^ (n - 1) * (MvPolynomial.pderiv i) f
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.rnDeriv_posterior_ae_prod : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] [inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧],
  (∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)) →
    ∀ᵐ (p : Ω × 𝓧) ∂μ.prod (μ.bind ⇑κ),
      (ProbabilityTheory.posterior κ μ).rnDeriv (ProbabilityTheory.Kernel.const 𝓧 μ) p.2 p.1 =
        κ.rnDeriv (ProbabilityTheory.Kernel.const Ω (μ.bind ⇑κ)) p.1 p.2
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reduce.eq_def : ∀ {m : ℤ} (A : FixedDetMatrix (Fin 2) ℤ m),
  FixedDetMatrices.reduce A =
    if ↑A 1 0 = 0 then
      if 0 < ↑A 0 0 then ModularGroup.T ^ (-(↑A 0 1 / ↑A 1 1)) • A
      else ModularGroup.T ^ (-(-↑A 0 1 / -↑A 1 1)) • ModularGroup.S • ModularGroup.S • A
    else FixedDetMatrices.reduce (FixedDetMatrices.reduceStep A)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhile.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : false = true → motive true) (h_2 : false = false → motive false),
  (match hP : false with
    | true => h_1 hP
    | false => h_2 hP) =
    h_2 ⋯
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitRightOpIsoOpColimit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.limitRightOpIsoOpColimit F =
    CategoryTheory.Limits.limit.isoLimitCone
      { cone := CategoryTheory.Limits.coneRightOpOfCocone (CategoryTheory.Limits.colimit.cocone F),
        isLimit := CategoryTheory.Limits.isLimitConeRightOpOfCocone F (CategoryTheory.Limits.colimit.isColimit F) }
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `J` is `u`-small, the forgetful functor from `AddGrpCat.{u}` preserves limits
of shape `J`.  -/
AddGrpCat.forget_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddGrpCat)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.sup_normal : ∀ {G : Type u_2} [inst : AddGroup G] (H K : AddSubgroup G) [hH : H.Normal] [hK : K.Normal], (H ⊔ K).Normal
-- Mathlib.GroupTheory.Commensurable
/-- Alias for the forward direction of `commensurable_conj` to allow dot-notation  -/
Subgroup.Commensurable.conj : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  H.Commensurable K → ∀ (g : ConjAct G), (g • H).Commensurable (g • K)
-- Aesop.Script.Step
Aesop.Script.mkOneBasedNumLit : ℕ → Lean.NumLit
-- Batteries.Data.List.Basic
List.takeD_nil : ∀ {α : Type u_1} (n : ℕ) (a : α), List.takeD n [] a = List.replicate n a
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.nonunits_inj : ∀ {K : Type u} [inst : Field K] {A B : ValuationSubring K}, A.nonunits = B.nonunits ↔ A = B