mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_apply_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), toIocMod hp a a = a + p
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three : ∀ {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₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ : C₁} {X₂ : C₂} {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃) (g : (F.obj X₁).obj X₂ ⟶ X₃),
  adj₂.homEquiv (CategoryTheory.CategoryStruct.comp g f₃) =
    CategoryTheory.CategoryStruct.comp (adj₂.homEquiv g) ((G.obj (Opposite.op X₁)).map f₃)
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.tendsto_support_normed_smallSets : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional ℝ E]
  [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] {ι : Type u_2} {φ : ι → ContDiffBump c} {l : Filter ι},
  Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0) →
    Filter.Tendsto (fun i => Function.support fun x => (φ i).normed μ x) l (nhds c).smallSets
-- Mathlib.Algebra.Ring.Commute
/-- **Alias** of `neg_one_sq`. -/
neg_one_pow_two : ∀ {R : Type u} [inst : Monoid R] [inst_1 : HasDistribNeg R], (-1) ^ 2 = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.id_whiskerLeft : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ'),
  CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft (CategoryTheory.Limits.CatCospanTransform.id F G) η =
    CategoryTheory.CategoryStruct.comp ψ.leftUnitor.hom (CategoryTheory.CategoryStruct.comp η ψ'.leftUnitor.inv)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.JPDecl.mk.injEq : ∀ (name : Lean.Name) (params : Array (Lean.Elab.Term.Do.Var × Bool)) (body : Lean.Elab.Term.Do.Code)
  (name_1 : Lean.Name) (params_1 : Array (Lean.Elab.Term.Do.Var × Bool)) (body_1 : Lean.Elab.Term.Do.Code),
  ({ name := name, params := params, body := body } = { name := name_1, params := params_1, body := body_1 }) =
    (name = name_1 ∧ params = params_1 ∧ body = body_1)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.comp_continuousAt_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h : X ≃ₜ Y) (f : Z → X) (z : Z), ContinuousAt (⇑h ∘ f) z ↔ ContinuousAt f z
-- Mathlib.Order.Filter.Map
Filter.bind.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (m : α → Filter β), f.bind m = (Filter.map m f).join
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_minKey?_eq_not_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey?.isSome = !t.isEmpty
-- Mathlib.Algebra.Group.Defs
AddRightCancelSemigroup.ext : ∀ {G : Type u} {x y : AddRightCancelSemigroup G}, Add.add = Add.add → x = y
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_right_mono : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R}, I ≤ J → ∀ (n : ℕ), I ^ n ≤ J ^ n
-- Mathlib.Order.Interval.Set.Image
StrictAntiOn.mapsTo_Ioc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictAntiOn f (Set.Icc a b) → Set.MapsTo f (Set.Ioc a b) (Set.Ico (f b) (f a))
-- Mathlib.Analysis.Complex.Basic
RCLike.norm_to_complex : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] (a : 𝕜), ‖↑(RCLike.re a) + ↑(RCLike.im a) * Complex.I‖ = ‖a‖
-- Mathlib.FieldTheory.Separable
Polynomial.nodup_roots : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, p.Separable → p.roots.Nodup
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.uniformSpace : (α : Type u_1) → [inst : UniformSpace α] → UniformSpace (UniformSpace.Completion α)
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_eq_emod : ∀ {a b : ℤ}, a.tmod b = a % b - ↑(if 0 ≤ a ∨ b ∣ a then 0 else b.natAbs)
-- Mathlib.Algebra.BigOperators.Ring.Finset
Nat.cast_sum : ∀ {R : Type u_4} {ι : Type u_5} [inst : AddCommMonoidWithOne R] (s : Finset ι) (f : ι → ℕ),
  ↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.HashMap.ofList l).getKey? k = none
-- Init.Data.Slice.Array.Iterator
_private.Init.Data.Slice.Array.Iterator.0.SubarrayIterator.instFinitelessRelation : {α : Type u} → Std.Iterators.FinitenessRelation (SubarrayIterator α) Id
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} {hom : M.X ⟶ N.X}
  {left_act_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actLeft hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X hom) N.actLeft)
      Bimod.Hom.left_act_hom._autoParam}
  {right_act_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actRight hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hom B.X) N.actRight)
      Bimod.Hom.right_act_hom._autoParam}
  {hom_1 : M.X ⟶ N.X}
  {left_act_hom_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actLeft hom_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X hom_1) N.actLeft)
      Bimod.Hom.left_act_hom._autoParam}
  {right_act_hom_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actRight hom_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hom_1 B.X) N.actRight)
      Bimod.Hom.right_act_hom._autoParam},
  { hom := hom, left_act_hom := left_act_hom, right_act_hom := right_act_hom } =
      { hom := hom_1, left_act_hom := left_act_hom_1, right_act_hom := right_act_hom_1 } →
    hom = hom_1
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.isUniversal : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.IsUniversal
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Consumes projections to parent structures, and runs `d` in the resulting context.
For example, if the current expression is `o.toB.toA`, runs `d` with `o` as the current expression.

If `explicit` is true, then does not consume parent projections for structures with parameters,
since these are implicit arguments.
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.withoutParentProjections : {α : Type} → Bool → Lean.PrettyPrinter.Delaborator.DelabM α → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.forget_createsLimitsOfShape : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget AddGrpCat)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, ContDiffOn 𝕜 0 f s ↔ ContinuousOn f s
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.apply_symm_apply : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁.IsometryEquiv Q₂) (x : M₂),
  f (f.symm x) = x
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.antitone : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [MeasureTheory.IsFiniteMeasure μ] {p q : ENNReal}, p ≤ q → MeasureTheory.Lp E q μ ≤ MeasureTheory.Lp E p μ
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
SimpleGraph.dart_card_eq_sum_degrees : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  Fintype.card G.Dart = ∑ v, G.degree v
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.bicategory_leftUnitor_inv_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} (f : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor f).inv.unop2 = (CategoryTheory.Bicategory.rightUnitor f.unop).inv
-- Mathlib.Order.Filter.CountablyGenerated
Filter.HasBasis.isCountablyGenerated : ∀ {α : Type u_1} {ι : Type u_4} [Countable ι] {f : Filter α} {p : ι → Prop} {s : ι → Set α},
  f.HasBasis p s → f.IsCountablyGenerated
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCommCStarAlgebra.toStarRing : {A : Type u_1} → [self : NonUnitalCommCStarAlgebra A] → StarRing A
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.binders : Lean.Elab.PreDefinition → Lean.Syntax
-- Mathlib.Data.Set.Sups
Set.infs_sups_subset_left : ∀ {α : Type u_2} [inst : DistribLattice α] (s t u : Set α), s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u
-- Mathlib.Data.FinEnum
/-- Any enumeration of a type with unique inhabitant has length 1.  -/
FinEnum.card_eq_one : ∀ (α : Type u) [inst : FinEnum α] [Unique α], FinEnum.card α = 1
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Turn a subalgebra satisfying `IsField` into an intermediate field.  -/
Subalgebra.toIntermediateField' : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → (S : Subalgebra K L) → IsField ↥S → IntermediateField K L
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.exponent_eq_zero_of_infinite : ∀ {α : Type u_1} [inst : Group α] [IsCyclic α] [Infinite α], Monoid.exponent α = 0
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedMap_mono : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α],
  Monotone (ConditionallyCompleteLinearOrderedField.inducedMap α β)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrp_id_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Int.Internal.Linear.instReprExpr_lean.repr : Int.Internal.Linear.Expr → ℕ → Std.Format
-- Mathlib.Data.Int.Bitwise
Int.bodd_subNatNat : ∀ (m n : ℕ), (Int.subNatNat m n).bodd = (m.bodd ^^ n.bodd)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.of_isIso_comp_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Z ⟶ Y) (f : Y ⟶ X) [CategoryTheory.IsIso f]
  [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp g f)], CategoryTheory.IsIso g
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.Lemmas.FindPos.0.String.Slice.Pos.prevn.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Mathlib.RingTheory.Valuation.Basic
/-- The support of a valuation `v : R → Γ₀` is the ideal of `R` where `v` vanishes.  -/
Valuation.supp : {R : Type u_3} →
  {Γ₀ : Type u_4} → [inst : CommRing R] → [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] → Valuation R Γ₀ → Ideal R
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Max α] →
      [inst_1 : Max β] →
        [inst_2 : Bot α] → [inst_3 : Bot β] → (toSupHom : SupHom α β) → toSupHom.toFun ⊥ = ⊥ → SupBotHom α β
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.pow_right_iff : ∀ {R : Type u} [inst : CommSemiring R] {x y : R} {m : ℕ}, 0 < m → (IsCoprime x (y ^ m) ↔ IsCoprime x y)
-- Mathlib.RingTheory.Derivation.MapCoeffs
Derivation.mapCoeffs_C : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (d : Derivation R A M) (x : A),
  d.mapCoeffs (Polynomial.C x) = PolynomialModule.single A 0 (d x)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the morphism on the middle objects  -/
CategoryTheory.ShortComplex.Hom.τ₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → S₁.Hom S₂ → (S₁.X₂ ⟶ S₂.X₂)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.instBialgebra : (R : Type u_1) →
  (A : Type u_3) →
    (M : Type u_8) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [Bialgebra R A] → [inst_3 : Monoid M] → Bialgebra R (MonoidAlgebra A M)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_setIntegral_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s →
        ∀ (A : Set γ),
          Filter.Tendsto (fun i => ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) Filter.atTop
            (nhds (∫ (x : γ) in A, κ.density ν a x s ∂ν a))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_cfcₙ_le : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : ℝ},
  (∀ x ∈ quasispectrum 𝕜 a, ‖f x‖ ≤ c) → ‖cfcₙ f a‖ ≤ c
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.function.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.function = 1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_roo_eq_fallback : ∀ {m n i fallback : ℕ}, n ≤ i + (m + 1) → (m<...n).toArray.getD i fallback = fallback
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toList_rco : ∀ {m n k : ℤ}, List.map (fun x => x + k) (m...n).toList = ((m + k)...n + k).toList
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measurableSet_Ioi : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) {c : R},
  MeasurableSet (Set.Ioi c)
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.stepOnQuotient_mk : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {β : Type w} [inst : Monad m] [inst_1 : LawfulMonad m]
  {bit : Std.BundledIterM m β},
  Std.BundledIterM.stepOnQuotient (Quot.mk (Std.BundledIterM.Equiv m β) bit) =
    Std.IterStep.mapIterator (Quot.mk (Std.BundledIterM.Equiv m β)) <$> bit.step
-- Init.Data.Int.Gcd
Int.lcm_eq_mul_iff : ∀ {m n : ℤ}, m.lcm n = m.natAbs * n.natAbs ↔ m = 0 ∨ n = 0 ∨ m.gcd n = 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `F` is fully faithful, then so is `Under.post F`.  -/
CategoryTheory.Functor.FullyFaithful.under : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (X : T) → (F : CategoryTheory.Functor T D) → F.FullyFaithful → (CategoryTheory.Under.post F).FullyFaithful
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.embeddingLike : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  EmbeddingLike (L.Embedding M N) M N
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.separatingLeft_iff_forall_vecMul_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Finite n], M.SeparatingLeft ↔ ∀ (v : m → R), Matrix.vecMul v M = 0 → v = 0
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.comp_le_of_antitoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {β : Type u_3}
  [inst_2 : LinearOrder β] (f : α → E) {s : Set α} {t : Set β} (φ : β → α),
  AntitoneOn φ t → Set.MapsTo φ t s → eVariationOn (f ∘ φ) t ≤ eVariationOn f s
-- Lean.Elab.BindersUtil
/-- Helper function for `expandEqnsIntoMatch`  -/
Lean.Elab.Term.getMatchAltsNumPatterns : Lean.Syntax → ℕ
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller₀_spec : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R},
  (∀ (n : ℕ), ∃ z, (Ideal.Quotient.mk I) z = (Perfection.coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) →
    (Perfection.teichmuller₀ p I) x = y
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (c : ENNReal),
  ∫⁻ (x : α) in s, c ∂μ = c * μ s
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.findDiscrRefinementPath.goType : Lean.Expr → Lean.Expr → OptionT Lean.MetaM (List ℕ)
-- Qq.Macro
/-- New unquoted local context  -/
Qq.Impl.UnquoteState.unquoted : Qq.Impl.UnquoteState → Lean.LocalContext
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_eq_ofNat : ∀ (n : ℕ) {h : n < UInt32.size}, UInt32.ofNatLT n h = UInt32.ofNat n
-- Mathlib.Analysis.Normed.Group.Basic
edist_one_left : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), edist 1 a = ↑‖a‖₊
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.find?_prop_eq_some_iff_splits : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String} {pos : s.Pos},
  s.find? p = some pos ↔ ∃ t c u, pos.Splits t (String.singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, ¬p d
-- Mathlib.LinearAlgebra.Eigenspace.Charpoly
Module.End.det_eq_prod_roots_charpoly_of_splits : ∀ {K : Type u_3} {V : Type u_4} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : Module.Finite K V] {f : Module.End K V},
  (LinearMap.charpoly f).Splits → LinearMap.det f = (LinearMap.charpoly f).roots.prod
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.coeMulHom_apply : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  (self : { x // x ∈ Set.Ico 0 1 }), Set.Ico.coeMulHom self = ↑self
-- Mathlib.Algebra.MvPolynomial.Cardinal
MvPolynomial.cardinalMk_eq : ∀ {σ R : Type u} [inst : CommSemiring R] [IsEmpty σ], Cardinal.mk (MvPolynomial σ R) = Cardinal.mk R
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.compare_getKey?_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, Option.all (fun x => decide (cmp x k = Ordering.eq)) (t.getKey? k) = true
-- Mathlib.GroupTheory.Congruence.Defs
/-- The map sending a congruence relation to its underlying binary relation is injective.  -/
Con.ext' : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, ⇑c = ⇑d → c = d
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.self_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k}
  {fallback : α}, (cmp k ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.Lean.Meta.CongrTheorems
/-- Like `subsingletonElim` but uses `FastSubsingleton` to fail fast.  -/
Lean.Meta.fastSubsingletonElim : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.homologyFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C] (n : ℕ) {X Y : SSet}
  (f : X ⟶ Y), (SSet.homologyFunctor R n).map f = SSet.homologyMap f R n
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.extend_eq_at' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] [T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (c : γ),
  Filter.Tendsto f (nhds a) (nhds c) → di.extend f (i a) = f a
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.spine_map_vertex : ∀ (X : SSet) (n : ℕ) (Δ : X.obj (Opposite.op { len := n })) {m : ℕ} (φ : { len := m } ⟶ { len := n }) (i : Fin (m + 1)),
  (X.spine m ((CategoryTheory.ConcreteCategory.hom (X.map φ.op)) Δ)).vertex i =
    (X.spine n Δ).vertex ((SimplexCategory.Hom.toOrderHom φ) i)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.ext_iff : ∀ {R : Type u_1} {x y : Cubic R}, x = y ↔ x.a = y.a ∧ x.b = y.b ∧ x.c = y.c ∧ x.d = y.d
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
AlgebraicGeometry.formallyUnramified_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.FormallyUnramified f ↔
    ∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FormallyUnramified
-- Mathlib.Algebra.Star.Unitary
Unitary.smul_mem_of_mem : ∀ {R : Type u_1} {A : Type u_2} [inst : Monoid R] [inst_1 : Monoid A] [inst_2 : MulAction R A] [SMulCommClass R A A]
  [IsScalarTower R A A] [inst_5 : StarMul R] [inst_6 : StarMul A] [StarModule R A] {r : R} {a : A},
  r ∈ unitary R → a ∈ unitary A → r • a ∈ unitary A
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.coeff_toSubring' : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) {n : ℕ},
  ↑((p.toSubring T hp).coeff n) = p.coeff n
-- Mathlib.Algebra.Lie.Abelian
LieModule.commute_toEnd_of_mem_center_left : ∀ {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] [inst_6 : LieModule R L M] {x : L},
  x ∈ LieAlgebra.center R L → ∀ (y : L), Commute ((LieModule.toEnd R L M) x) ((LieModule.toEnd R L M) y)
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- Given a manifold with a Riemannian metric, consider the associated Riemannian distance. Then
by definition the distance is the infimum of the length of paths between the points, i.e., the
manifold satisfies the `IsRiemannianManifold I M` predicate.  -/
instIsRiemannianManifold : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [inst_7 : IsContinuousRiemannianBundle E fun x => TangentSpace I x] [inst_8 : RegularSpace M],
  IsRiemannianManifold I M
-- Mathlib.Data.Finset.NAry
Finset.inf_image₂_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α)
  (t : Finset β) [inst_1 : SemilatticeInf δ] [inst_2 : OrderTop δ] (g : γ → δ),
  (Finset.image₂ f s t).inf g = t.inf fun y => s.inf fun x => g (f x y)