mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.BitVec.Lemmas
BitVec.msb_setWidth : ∀ {w v : ℕ} (x : BitVec w), (BitVec.setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_Φ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [Nontrivial R] (n : ℤ), (W.Φ n).natDegree = n.natAbs ^ 2
-- Mathlib.Data.Finsupp.AList
AList.lookupFinsupp_support : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : DecidableEq α] [inst_2 : DecidableEq M]
  (l : AList fun _x => M), l.lookupFinsupp.support = (List.filter (fun x => decide (x.snd ≠ 0)) l.entries).keys.toFinset
-- Mathlib.RingTheory.TensorProduct.Maps
/-- Algebra maps `S ⊗[R] B →ₐ[S] C` are the same as algebra maps `B →ₐ[R] C`.
Variant of `Algebra.TensorProduct.liftEquiv` where the left map is fixed.
 -/
Algebra.TensorProduct.liftEquivRight : (R : Type uR) →
  (S : Type uS) →
    (B : Type uB) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R B] →
                (C : Type u_3) →
                  [inst_5 : CommRing C] →
                    [inst_6 : Algebra R C] →
                      [inst_7 : Algebra S C] → [IsScalarTower R S C] → (B →ₐ[R] C) ≃ (TensorProduct R S B →ₐ[S] C)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
AnalyticOn.rexp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  AnalyticOn ℝ f s → AnalyticOn ℝ (fun z => Real.exp (f z)) s
-- Lean.Data.Lsp.Extra
Lean.Lsp.instBEqLeanFileProgressKind : BEq Lean.Lsp.LeanFileProgressKind
-- Mathlib.Algebra.Group.Defs
/-- One is a right neutral element for multiplication  -/
Monoid.mul_one : ∀ {M : Type u} [self : Monoid M] (a : M), a * 1 = a
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_sup_sub_sup_le_abs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b c : α), |a ⊔ c - b ⊔ c| ≤ |a - b|
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.nonempty_iff_ne_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C), P.Nonempty ↔ ¬P = ⊥
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM_keysArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldrM (fun a x d => f a d) init t = Array.foldrM f init t.keysArray
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_iff_nat : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : ℕ∞}, ContMDiffWithinAt I I' (↑n) f s x ↔ ∀ (m : ℕ), ↑m ≤ n → ContMDiffWithinAt I I' (↑m) f s x
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.baseEmbedding_strictMono : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R) [IsOrderedAddMonoid R],
  StrictMono ↑seed.baseEmbedding
-- Mathlib.Order.InitialSeg
PrincipalSeg.instIsEmptyOfIsWellOrder : ∀ {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r], IsEmpty (PrincipalSeg r r)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Isomorphic rings have isomorphic additive monoid algebras.  -/
AddMonoidAlgebra.mapRingEquiv : {R : Type u_3} →
  {S : Type u_4} →
    (M : Type u_6) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : AddMonoid M] → R ≃+* S → AddMonoidAlgebra R M ≃+* AddMonoidAlgebra S M
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.smul_eq_C_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R) (a : R), a • p = MvPolynomial.C a * p
-- Init.Data.Vector.Lemmas
Vector.map_flatMap : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {m n : ℕ} {f : β → γ} {g : α → Vector β m} {xs : Vector α n},
  Vector.map f (xs.flatMap g) = xs.flatMap fun a => Vector.map f (g a)
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.merge.match_1.eq_3 : ∀ {α : Type u_1} (motive : Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α → Sort u_2) (a₁ : α)
  (c₁ sibling : Batteries.PairingHeapImp.Heap α)
  (h_1 : Unit → motive Batteries.PairingHeapImp.Heap.nil Batteries.PairingHeapImp.Heap.nil)
  (h_2 :
    (a₂ : α) →
      (c₂ sibling : Batteries.PairingHeapImp.Heap α) →
        motive Batteries.PairingHeapImp.Heap.nil (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling))
  (h_3 :
    (a₁ : α) →
      (c₁ sibling : Batteries.PairingHeapImp.Heap α) →
        motive (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling) Batteries.PairingHeapImp.Heap.nil)
  (h_4 :
    (a₁ : α) →
      (c₁ sibling : Batteries.PairingHeapImp.Heap α) →
        (a₂ : α) →
          (c₂ sibling_1 : Batteries.PairingHeapImp.Heap α) →
            motive (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling)
              (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_1)),
  (match Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling, Batteries.PairingHeapImp.Heap.nil with
    | Batteries.PairingHeapImp.Heap.nil, Batteries.PairingHeapImp.Heap.nil => h_1 ()
    | Batteries.PairingHeapImp.Heap.nil, Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling => h_2 a₂ c₂ sibling
    | Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling, Batteries.PairingHeapImp.Heap.nil => h_3 a₁ c₁ sibling
    | Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling, Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_1 =>
      h_4 a₁ c₁ sibling a₂ c₂ sibling_1) =
    h_3 a₁ c₁ sibling
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.inner_single_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι) (a : 𝕜)
  (v : EuclideanSpace 𝕜 ι), inner 𝕜 (EuclideanSpace.single i a) v = (starRingEnd 𝕜) a * v.ofLp i
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Fintype.piFinset_vadd_finset : ∀ {ι : Type u_5} {α : ι → Type u_6} {β : ι → Type u_7} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (β i)] [inst_3 : (i : ι) → VAdd (α i) (β i)] (a : (i : ι) → α i)
  (s : (i : ι) → Finset (β i)), (Fintype.piFinset fun i => a i +ᵥ s i) = a +ᵥ Fintype.piFinset s
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.instMulAction.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (H : Subgroup G),
  MulAction.instMulAction H =
    { toSemigroupAction := (Submonoid.instMulActionSubtypeMem H).toSemigroupAction, one_smul := ⋯ }
-- Mathlib.Data.Set.Lattice.Image
Set.preimage_iInter : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {s : ι → Set β}, f ⁻¹' ⋂ i, s i = ⋂ i, f ⁻¹' s i
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- If the symmetric difference of two negative sets is a null-set, then so are the differences
between the two sets.  -/
MeasureTheory.SignedMeasure.of_sdiff_eq_zero_of_symmDiff_eq_zero_negative : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v : Set α},
  MeasurableSet u →
    MeasurableSet v →
      MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u →
        MeasureTheory.VectorMeasure.restrict s v ≤ MeasureTheory.VectorMeasure.restrict 0 v →
          s (symmDiff u v) = 0 → s (u \ v) = 0 ∧ s (v \ u) = 0
-- Init.Data.SInt.Bitwise
ISize.neg_one_shiftLeft_and_shiftLeft : ∀ {a b : ISize}, (-1) <<< b &&& a <<< b = a <<< b
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- If `S` has Dirichlet density `δ`, then `dirichletDensity S = δ`.  -/
NumberField.Set.HasDirichletDensity.dirichletDensity_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ},
  NumberField.Set.HasDirichletDensity S δ → NumberField.Set.dirichletDensity S = δ
-- Mathlib.Data.List.Destutter
/-- `List.destutter'` on a relation like ≠, whose negation is an equivalence, has length
monotonic under List.cons  -/
List.le_length_destutter'_cons : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] {a b : α} [IsEquiv α Rᶜ] {l : List α},
  (List.destutter' R b l).length ≤ (List.destutter' R a (b :: l)).length
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.locallySmall_of_small_arrow : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [Small.{w, max u v} (CategoryTheory.Arrow C)],
  CategoryTheory.LocallySmall.{w, v, u} C
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.id_apply : ∀ {R : Type u} [inst : CommRing R] (A : CommHopfAlgCat R) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a
-- Mathlib.Order.Disjointed
disjointed_zero : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (f : ℕ → α), disjointed f 0 = f 0
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.nlt : ℕ → ℕ → Lean.Expr → Mathlib.Tactic.Order.AtomicFact
-- Init.System.IO
IO.instOrdTaskState.ord : IO.TaskState → IO.TaskState → Ordering
-- Mathlib.NumberTheory.ZetaValues
/-- The `0`-th Fourier coefficient of `Bₖ(x)`.  -/
bernoulliFourierCoeff_zero : ∀ {k : ℕ}, k ≠ 0 → bernoulliFourierCoeff k 0 = 0
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.uniqueAlgEquiv_symm_apply : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] [inst_4 : Subsingleton M] (a : A),
  (AddMonoidAlgebra.uniqueAlgEquiv R M).symm a = AddMonoidAlgebra.single 0 a
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_smulRight : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {M₁ : Type u_5} {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁]
  [inst_6 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [inst_7 : Finite m] (f : M₁ →ₗ[R] R)
  (x : M₂), (LinearMap.toMatrix v₁ v₂) (f.smulRight x) = Matrix.vecMulVec (⇑(v₂.repr x)) (⇑f ∘ ⇑v₁)
-- Mathlib.Algebra.Torsor.Basic
/-- If dividing two points by the same point produces equal results, those points are equal.  -/
sdiv_left_cancel : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {p₁ p₂ p : P}, p₁ /ₛ p = p₂ /ₛ p → p₁ = p₂
-- Init.Data.Ord.SInt
ISize.instLawfulOrderOrd : Std.LawfulOrderOrd ISize
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_functor_obj_mon_mul_unmop : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Mon C), CategoryTheory.MonObj.mul.unmop = CategoryTheory.MonObj.mul
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.map_id : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (n : ℕ),
  ContinuousCohomology.map (ContinuousMonoidHom.id G) (CategoryTheory.CategoryStruct.id X) n =
    CategoryTheory.CategoryStruct.id (continuousCohomology n X)
-- Mathlib.Algebra.Regular.Defs
/-- A regular element is an element `c` such that multiplication by `c` both on the left and
on the right is injective.  -/
IsRegular : {R : Type u_1} → [Mul R] → R → Prop
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.even.lift.aux_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : CliffordAlgebra.EvenHom Q A)
  (m₁ m₂ : M), (CliffordAlgebra.even.lift.aux f) (((CliffordAlgebra.even.ι Q).bilin m₁) m₂) = (f.bilin m₁) m₂
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk' : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  (x : Quotient (Submodule.quotientRel (IsLocalRing.maximalIdeal (ArchimedeanClass.FiniteElement K)))),
  (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (ArchimedeanClass.FiniteElement K))) ⁻¹'
      {x}).OrdConnected
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- A family of seminorms inducing a T₁ topology is separating.  -/
WithSeminorms.separating_of_T1 : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} [T1Space E],
  WithSeminorms p → ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0
-- Mathlib.Data.PNat.Prime
PNat.gcd_eq_left_iff_dvd : ∀ {m n : ℕ+}, m.gcd n = m ↔ m ∣ n
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Variant of `e.map_source` and `map_source'`, stated for images of subsets of `source`.  -/
PartialEquiv.image_source_subset : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), ↑e '' e.source ⊆ e.target
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalCase' : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
/-- Linear maps which are completely positive are order homomorphisms (i.e., positive maps).  -/
OrderHomClass.of_map_cstarMatrix_nonneg : ∀ {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂]
  [inst_6 : FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂],
  (∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ) → OrderHomClass F A₁ A₂
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Limits.exists_hom_of_preservesColimit_yoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone D}
  (hc : CategoryTheory.Limits.IsLimit c) {X : C}
  [CategoryTheory.Limits.PreservesColimit D.op (CategoryTheory.yoneda.obj X)] (f : c.pt ⟶ X),
  ∃ j p, CategoryTheory.CategoryStruct.comp (c.π.app j) p = f
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.ins.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertList_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.containsKey k toInsert = true →
        Std.Internal.List.getKeyD k (Std.Internal.List.insertList l toInsert) fallback =
          Std.Internal.List.getKeyD k toInsert fallback
-- Init.Data.Int.DivMod.Lemmas
Int.neg_mul_bmod_right : ∀ (a : ℕ) (b : ℤ), (-(↑a * b)).bmod a = 0
-- Mathlib.Data.Finset.Card
Finset.card_sdiff_add_card_eq_card : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s ⊆ t → (t \ s).card + s.card = t.card
-- Mathlib.Order.Basic
compl_gt : ∀ {α : Type u_2} [inst : LinearOrder α], (fun x1 x2 => x1 > x2)ᶜ = fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Regular.Defs
/-- An add-right-regular element is an element `c` such that addition
on the right by `c` is injective.  -/
IsAddRightRegular : {R : Type u_1} → [Add R] → R → Prop
-- Mathlib.NumberTheory.Primorial
primorial_dvd_primorial : ∀ {m n : ℕ}, m ≤ n → primorial m ∣ primorial n
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.isPartitionSplit : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι) (x : ℝ), (BoxIntegral.Prepartition.split I i x).IsPartition
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instMin.eq_1 : ∀ (M : Type u_1) [inst : MulOneClass M],
  SaturatedSubmonoid.instMin M =
    {
      min := fun s₁ s₂ =>
        let __src := s₁.toSubmonoid ⊓ s₂.toSubmonoid;
        { toSubmonoid := __src, mulSaturated := ⋯ } }
-- Mathlib.RingTheory.Finiteness.Descent
/-- If `T ⊗[R] S` is of finite presentation over `T` and `T` is `R`-faithfully flat,
then `S` is of finite presentation over `R`  -/
Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.FaithfullyFlat R T]
  [Algebra.FinitePresentation T (TensorProduct R T S)], Algebra.FinitePresentation R S
-- Mathlib.Algebra.GCDMonoid.Basic
/-- **Alias** of `strongNormalizationMonoidOfMonoidHomRightInverse`.

---

Define `NormalizationMonoid` on a structure from a `MonoidHom` inverse to `Associates.mk`.  -/
normalizationMonoidOfMonoidHomRightInverse : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [DecidableEq α] → (f : Associates α →* α) → Function.RightInverse (⇑f) Associates.mk → StrongNormalizationMonoid α
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.ExprWithAnchor.mk : Lean.Expr → UInt64 → Lean.Meta.Grind.ExprWithAnchor
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.ofIso_symm : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module R Y] {Q₁ : QuadraticForm R X} {Q₂ : QuadraticForm R Y}
  (e : QuadraticMap.IsometryEquiv Q₁ Q₂), QuadraticModuleCat.ofIso e.symm = (QuadraticModuleCat.ofIso e).symm
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- The averaging of a uniformly integrable real-valued sequence is also uniformly integrable.  -/
MeasureTheory.uniformIntegrable_average_real : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal},
  1 ≤ p →
    ∀ {f : ℕ → α → ℝ},
      MeasureTheory.UniformIntegrable f p μ →
        MeasureTheory.UniformIntegrable (fun n => (∑ i ∈ Finset.range n, f i) / ↑n) p μ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_iff_pos_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (a : α) {b : α},
  a < a + b ↔ 0 < b
-- Mathlib.Combinatorics.Additive.FreimanHom
isAddFreimanIso_one_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsAddFreimanIso 1 A B f ↔ Set.BijOn f A B
-- Mathlib.Algebra.GroupWithZero.Defs
SemigroupWithZero.mk : {S₀ : Type u} →
  [toSemigroup : Semigroup S₀] →
    [toZero : Zero S₀] → (∀ (a : S₀), 0 * a = 0) → (∀ (a : S₀), a * 0 = 0) → SemigroupWithZero S₀
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.setTermRingId : Lean.Expr → Lean.Meta.Grind.Arith.CommRing.RingM Unit
-- Mathlib.Data.Setoid.Partition
/-- A finite setoid partition furnishes a finpartition  -/
Setoid.IsPartition.finpartition : {α : Type u_1} → {c : Finset (Set α)} → Setoid.IsPartition ↑c → Finpartition Set.univ
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- Two finite-dimensional topological vector spaces over a complete normed field are continuously
linearly equivalent if and only if they have the same (finite) dimension.  -/
FiniteDimensional.nonempty_continuousLinearEquiv_iff_finrank_eq : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [inst_5 : AddCommGroup F]
  [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜]
  [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F],
  Nonempty (E ≃L[𝕜] F) ↔ Module.finrank 𝕜 E = Module.finrank 𝕜 F
-- Lean.LocalContext
/-- Is the local declaration an implementation-detail hypothesis
(including auxiliary declarations)?
 -/
Lean.LocalDecl.isImplementationDetail : Lean.LocalDecl → Bool
-- Mathlib.Data.Int.Order.Units
Int.units_coe_mul_self : ∀ (u : ℤˣ), ↑u * ↑u = 1
-- Mathlib.Data.Finite.Prod
AddEquiv.finite_right : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β] [Finite β], Finite (α ≃+ β)
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.contains a = false
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- The value of `χ₄ n`, for `n : ℤ`, depends only on `n % 4`.  -/
ZMod.χ₄_int_mod_four : ∀ (n : ℤ), ZMod.χ₄ ↑n = ZMod.χ₄ ↑(n % 4)
-- Mathlib.Algebra.Module.Submodule.Invariant
Sublattice.mk.congr_simp : ∀ {α : Type u_2} [inst : Lattice α] (carrier carrier_1 : Set α) (e_carrier : carrier = carrier_1)
  (supClosed' : SupClosed carrier) (infClosed' : InfClosed carrier),
  { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' } =
    { carrier := carrier_1, supClosed' := ⋯, infClosed' := ⋯ }
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAt.sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F},
  (∀ i ∈ u, HasDerivAt (A i) (A' i) x) → HasDerivAt (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAdd : {α : Type u_1} → [Add α] → Add (Lex α)
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LiftSourceTargetPropertyAt.mem_domChart_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (h : Manifold.LiftSourceTargetPropertyAt I J n f x P), x ∈ h.domChart.source
-- Mathlib.Logic.Equiv.Defs
Equiv.conj_apply : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (f : α → α) (a : β), e.conj f a = e (f (e.symm a))
-- Init.Data.BitVec.Lemmas
BitVec.toFin_or : ∀ {v : ℕ} (x y : BitVec v), (x ||| y).toFin = x.toFin ||| y.toFin
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : CategoryTheory.SimplicialObject.Augmented C),
  (AlgebraicTopology.AlternatingFaceMapComplex.ε.app X).f 0 = X.hom.app (Opposite.op { len := 0 })
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.toScott_symm_eq : ∀ {α : Type u_1}, Topology.WithScott.toScott.symm = Topology.WithScott.ofScott
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.mapDomainLinearMap_single : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (f : M → N) (s : S) (m : M),
  (MonoidAlgebra.mapDomainLinearMap R S f) (MonoidAlgebra.single m s) = MonoidAlgebra.single (f m) s
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCMRight_dvd_right : ∀ (a b : ℕ), a.factorizationLCMRight b ∣ b