mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyLT!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLT! k = t₂.getKeyLT! k
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The equivalence `(X ⊗ Y).HomotopyCategory ≌ X.HomotopyCategory ⥤ Y.HomotopyCategory`
when `X` and `Y` are `2`-truncated simplicial sets.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.equivalence : (X Y : SSet.Truncated 2) →
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory ≌ X.HomotopyCategory × Y.HomotopyCategory
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNat.raw_refl : ∀ (n : ℕ), Mathlib.Meta.NormNum.IsNat n n
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `CommRing` instance along an injective function.  -/
Function.Injective.commRing : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : Neg S] →
                  [inst_5 : Sub S] →
                    [inst_6 : SMul ℕ S] →
                      [inst_7 : SMul ℤ S] →
                        [inst_8 : Pow S ℕ] →
                          [inst_9 : NatCast S] →
                            [inst_10 : IntCast S] →
                              [inst_11 : CommRing R] →
                                f 0 = 0 →
                                  f 1 = 1 →
                                    (∀ (x y : S), f (x + y) = f x + f y) →
                                      (∀ (x y : S), f (x * y) = f x * f y) →
                                        (∀ (x : S), f (-x) = -f x) →
                                          (∀ (x y : S), f (x - y) = f x - f y) →
                                            (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                              (∀ (n : ℤ) (x : S), f (n • x) = n • f x) →
                                                (∀ (x : S) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                  (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → CommRing S
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right_split_ineq : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly) (k : ℕ) (a : ℤ)
  (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_right_split ctx p₁ p₂ k →
    Int.Internal.Linear.cooper_right_split_ineq_cert p₁ p₂ (↑k) a p' = true →
      Int.Internal.Linear.Poly.denote' ctx p' ≤ 0
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_two_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] {J : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} J]
  [inst_4 :
    ∀ (F₁ F₂ : CategoryTheory.Functor J C), CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂]
  {F₁ F₂ F₂' F₃ : CategoryTheory.Functor J C} (f₂ : F₂ ⟶ F₂')
  (g : F₂' ⟶ CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom C F₁ F₃),
  CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv.symm (CategoryTheory.CategoryStruct.comp f₂ g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft F₁ f₂)
      (CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv.symm g)
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `i : K →+* L` is a `p`-radical ring homomorphism, then it makes `L` a perfect closure
of `K`, if `L` is perfect.
In this case the kernel of `i` is equal to the `p`-nilradical of `K`
(see `IsPerfectClosure.ker_eq`).

Our definition makes it synonymous to `IsPRadical` if `PerfectRing L p` is present. A caveat is
that you need to write `[PerfectRing L p] [IsPerfectClosure i p]`. This is similar to
`PerfectRing` which has `ExpChar` as a prerequisite.  -/
IsPerfectClosure : {K : Type u_1} →
  {L : Type u_2} →
    [inst : CommSemiring K] → [inst_1 : CommSemiring L] → (K →+* L) → (p : ℕ) → [ExpChar L p] → [PerfectRing L p] → Prop
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_sdiff' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasureTheory.NullMeasurableSet t μ → μ t ≠ ⊤ → μ (s \ t) = μ (s ∪ t) - μ t
-- Mathlib.Algebra.Homology.SingleHomology
/-- The canonical isomorphism `((single C c j).obj A).cycles j ≅ A`  -/
HomologicalComplex.singleObjCyclesSelfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {ι : Type u_1} →
          [inst_3 : DecidableEq ι] →
            (c : ComplexShape ι) → (j : ι) → (A : C) → ((HomologicalComplex.single C c j).obj A).cycles j ≅ A
-- Aesop.Rule.Name
Aesop.instInhabitedBuilderName.default : Aesop.BuilderName
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- Natural isomorphism needed in the construction of `equivalenceSelfOfHasFiniteBiproducts`.
 -/
CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproductsAux : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] →
        (CategoryTheory.Mat_.embedding C).comp (CategoryTheory.Functor.id (CategoryTheory.Mat_ C)) ≅
          (CategoryTheory.Mat_.embedding C).comp
            ((CategoryTheory.Mat_.lift (CategoryTheory.Functor.id C)).comp (CategoryTheory.Mat_.embedding C))
-- Mathlib.CategoryTheory.Generator.Preadditive
CategoryTheory.isSeparator_iff_faithful_preadditiveCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (G : C),
  CategoryTheory.IsSeparator G ↔ (CategoryTheory.preadditiveCoyoneda.obj (Opposite.op G)).Faithful
-- Mathlib.RingTheory.Algebraic.MvPolynomial
MvPolynomial.transcendental_supported_polynomial_aeval_X : ∀ {σ : Type u_1} (R : Type u_2) [inst : CommRing R] {i : σ} {s : Set σ},
  i ∉ s →
    ∀ {f : Polynomial R},
      Transcendental R f → Transcendental (↥(MvPolynomial.supported R s)) ((Polynomial.aeval (MvPolynomial.X i)) f)
-- Mathlib.Topology.Algebra.Ring.Basic
/-- If a non-unital subsemiring of a non-unital topological semiring is commutative, then so is its
topological closure.

See note [reducible non-instances]  -/
NonUnitalSubsemiring.nonUnitalCommSemiringTopologicalClosure : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalSemiring R] →
      [inst_2 : IsSemitopologicalSemiring R] →
        [T2Space R] →
          (s : NonUnitalSubsemiring R) → (∀ (x y : ↥s), x * y = y * x) → NonUnitalCommSemiring ↥s.topologicalClosure
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.List.ProveNilOrConsResult.nil.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(List «$α»)} {pf pf_1 : Q(«$s» = [])},
  Mathlib.Meta.List.ProveNilOrConsResult.nil pf = Mathlib.Meta.List.ProveNilOrConsResult.nil pf_1 → pf = pf_1
-- Mathlib.Analysis.MeanInequalities
/-- **Young's inequality** equality condition, `ℝ≥0` version with real conjugate exponents.  -/
NNReal.young_inequality_real_eq_iff : ∀ (a b : NNReal) {p q : ℝ}, p.HolderConjugate q → (a * b = a ^ p / p.toNNReal + b ^ q / q.toNNReal ↔ a ^ p = b ^ q)
-- Lean.Meta.Tactic.Delta
Lean.Meta.delta? : Lean.Expr → (optParam (Lean.Name → Bool) fun x => true) → optParam Bool false → Lean.CoreM (Option Lean.Expr)
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageParams.mk.sizeOf_spec : ∀ (type : Lean.Lsp.MessageType) (message : String),
  sizeOf { type := type, message := message } = 1 + sizeOf type + sizeOf message
-- Mathlib.Analysis.Convex.Segment
segment_eq_uIcc : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y : 𝕜),
  segment 𝕜 x y = Set.uIcc x y
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getDₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] (k : α)
  (l : Std.DTreeMap.Internal.Impl α β) (fallback : β k),
  Std.DTreeMap.Internal.Impl.getDₘ k l fallback = (l.get?ₘ k).getD fallback
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The inf of two subsemigroups is their intersection.  -/
Subsemigroup.instMin : {M : Type u_1} → [inst : Mul M] → Min (Subsemigroup M)
-- Mathlib.Analysis.CStarAlgebra.Fuglede
/-- **Alias** of `SemiconjBy.star_right`.

---

**Fuglede–Putnam–Rosenblum**: If `a` and `b` are normal elements in a C⋆-algebra `A` which
are interwined by `x`, then `star a` and `star b` are also intertwined by `x`.  -/
fuglede_putnam_rosenblum : ∀ {A : Type u_2} [inst : NonUnitalCStarAlgebra A] {a b x : A},
  IsStarNormal a → IsStarNormal b → SemiconjBy x a b → SemiconjBy x (star a) (star b)
-- Mathlib.Data.Part
Part.subsingleton : ∀ {α : Type u_1} (o : Part α), {a | a ∈ o}.Subsingleton
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.AlternatingMap.ext_iff : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} {φ φ' : M.AlternatingMap N n},
  φ = φ' ↔ ∀ (x : Fin n → ↑M), φ x = φ' x
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_le_one_of_one_le_of_nonpos : ∀ {x : NNReal} {z : ℝ}, 1 ≤ x → z ≤ 0 → x ^ z ≤ 1
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {l : List α} {k k' : α},
  (k == k') = true → k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertMany l).get! k' = k
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.int_cyclotomic_unique : ∀ {n : ℕ} {P : Polynomial ℤ},
  Polynomial.map (Int.castRingHom ℂ) P = Polynomial.cyclotomic' n ℂ → P = Polynomial.cyclotomic n ℤ
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.charpoly_def : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M),
  f.charpoly = ((LinearMap.toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M)) f).charpoly
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'.match_3.splitter : {m : Type u_1 → Type u_2} →
  {α β : Type u_1} →
    [inst : Std.Iterator α m β] →
      (it : Std.IterM m β) →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Lean.Meta.ExprLens
_private.Lean.Meta.ExprLens.0.Lean.Meta.foldAncestorsAux : {M : Type → Type} →
  [Monad M] →
    [MonadLiftT Lean.MetaM M] →
      [MonadControlT Lean.MetaM M] →
        [Lean.MonadError M] →
          {α : Type} → (Array Lean.Expr → Lean.Expr → ℕ → α → M α) → α → List ℕ → Array Lean.Expr → Lean.Expr → M α
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instDivisionMonoid : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [DivisionMonoid G] → DivisionMonoid (l.Germ G)
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- The `K`-algebra equivalence between `K⟮X⟯` and an intermediate field `E` given
by sending `X` to `generator E`. See also `Luroth.eq_adjoin_generator`.  -/
RatFunc.Luroth.algEquiv : {K : Type u_1} → [inst : Field K] → {E : IntermediateField K (RatFunc K)} → E ≠ ⊥ → RatFunc K ≃ₐ[K] ↥E
-- Init.Data.BitVec.Lemmas
BitVec.sdiv_eq_and : ∀ (x y : BitVec 1), x.sdiv y = x &&& y
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.instMulActionAut : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → MulAction P.Aut ι
-- Mathlib.Algebra.Ring.Hom.Defs
RingHomClass.toNonUnitalRingHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] {x : NonAssocSemiring α}
  {x_1 : NonAssocSemiring β} [RingHomClass F α β], NonUnitalRingHomClass F α β
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment.eq_3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.addPosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.eq_of_isBasis : ∀ {α : Type u_1} {M : Matroid α} {I J : Set α}, M.Indep I → M.IsBasis J I → J = I
-- Init.SimpLemmas
Bool.not_eq_true : ∀ (b : Bool), (¬b = true) = (b = false)
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.toPreadditive : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} → [self : CategoryTheory.Abelian C] → CategoryTheory.Preadditive C
-- Init.Data.String.PosRaw
String.Pos.Raw.ne_of_lt : ∀ {a b : String.Pos.Raw}, a < b → a ≠ b
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.p_descOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
  (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0),
  CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.descOpcycles k j hj hk) = k
-- Mathlib.Data.Nat.Find
Nat.le_findGreatest : ∀ {m : ℕ} {P : ℕ → Prop} [inst : DecidablePred P] {n : ℕ}, m ≤ n → P m → m ≤ Nat.findGreatest P n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_vert_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} [CategoryTheory.IsIso g] [CategoryTheory.IsIso inl],
  CategoryTheory.CommSq f g inl inr → CategoryTheory.IsPushout f g inl inr
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- A variant of `IsHausdorff.funext`, where the target is a ring instead of a module.
 -/
IsHausdorff.funext' : ∀ {R : Type u_6} {S : Type u_7} [inst : CommRing S] (I : Ideal S) [IsHausdorff I S] {f g : R → S},
  (∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ n)) (f r) = (Ideal.Quotient.mk (I ^ n)) (g r)) → f = g
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.bot_ne_one : ∀ {α : Type u} [inst : One α], ⊥ ≠ 1
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.countKnown.go : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → {len : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec len → ℕ → ℕ → ℕ
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.withTopOrderIso.eq_1 : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  FiniteMulArchimedeanClass.withTopOrderIso M = WithTop.subtypeOrderIso
-- Mathlib.Algebra.Order.AddTorsor
/-- An ordered vector addition is a bi-monotone vector addition.  -/
IsOrderedVAdd : (G : Type u_3) → (P : Type u_4) → [LE G] → [LE P] → [VAdd G P] → Prop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)},
  (m.alter k f).get? k' = if h : (k == k') = true then cast ⋯ (f (m.get? k)) else m.get? k'
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_trace : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : Fintype n] [inst_3 : AddCommMonoid R] [ContinuousAdd R] {A : X → Matrix n n R},
  Continuous A → Continuous fun x => (A x).trace
-- Mathlib.Topology.Constructions.SumProd
mem_nhds_prod_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x : X} {y : Y} {s : Set (X × Y)},
  s ∈ nhds (x, y) ↔ ∃ u ∈ nhds x, ∃ v ∈ nhds y, u ×ˢ v ⊆ s
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNorm_lsmul_apply_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_3} [inst_3 : SeminormedRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : IsBoundedSMul R E] [inst_7 : IsScalarTower 𝕜 R E] (x : R),
  ‖(ContinuousLinearMap.lsmul 𝕜 R) x‖ ≤ ‖x‖
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- The identity morphism lies in the structure groupoid.  -/
StructureGroupoid.id_mem' : ∀ {H : Type u_2} [inst : TopologicalSpace H] (self : StructureGroupoid H), OpenPartialHomeomorph.refl H ∈ self.members
-- Lean.Elab.Tactic.Omega.Core
/-- The number of new constraints that would be introduced by Fourier-Motzkin elimination.  -/
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.size : Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData → ℕ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α},
      Array.find? (fun x => cmp x.1 k == Ordering.eq) (Std.DTreeMap.Raw.Const.toArray t) = none ↔ t.contains k = false
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet : ∀ {G : Type u_1} {α : Type u_2} [inst : Zero G] [inst_1 : VAdd G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : autoParam (MeasureTheory.Measure α) MeasureTheory.IsAddFundamentalDomain._auto_1},
  MeasureTheory.IsAddFundamentalDomain G s μ → MeasureTheory.NullMeasurableSet s μ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_eq_cons_iff : ∀ {xs : List ℕ} {n a : ℕ}, (*...n).toList = a :: xs ↔ 0 = a ∧ 0 < n ∧ (1...n).toList = xs
-- Mathlib.Algebra.Group.Action.Pretransitive
MulAction.surjective_smul : ∀ (M : Type u_1) {α : Type u_3} [inst : SMul M α] [MulAction.IsPretransitive M α] (x : α),
  Function.Surjective fun c => c • x
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- Consider a multivariate polynomial `φ` whose variables are indexed by `Option σ`,
and suppose that `σ ≃ Fin n`.
Then one may view `φ` as a polynomial over `MvPolynomial (Fin n) R`, by

1. renaming the variables via `Option σ ≃ Fin (n+1)`, and then singling out the `0`-th variable
    via `MvPolynomial.finSuccEquiv`;
2. first viewing it as polynomial over `MvPolynomial σ R` via `MvPolynomial.optionEquivLeft`,
    and then renaming the variables.

This lemma shows that both constructions are the same.  -/
MvPolynomial.finSuccEquiv_rename_finSuccEquiv : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {n : ℕ} (e : σ ≃ Fin n) (φ : MvPolynomial (Option σ) R),
  (MvPolynomial.finSuccEquiv R n) ((MvPolynomial.rename ⇑(e.optionCongr.trans (finSuccEquiv n).symm)) φ) =
    Polynomial.map (MvPolynomial.rename ⇑e).toRingHom ((MvPolynomial.optionEquivLeft R σ) φ)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- We can pull out a product over a list in the first argument of the Jacobi symbol.  -/
jacobiSym.list_prod_left : ∀ {l : List ℤ} {n : ℕ}, jacobiSym l.prod n = (List.map (fun a => jacobiSym a n) l).prod
-- Mathlib.Algebra.Module.Presentation.Tensor
/-- The tensor product of two modules admits a presentation by generators and relations.  -/
Module.Relations.Solution.isPresentationCoreTensor : {A : Type u} →
  [inst : CommRing A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module A M₁] →
              [inst_4 : Module A M₂] →
                {relations₁ : Module.Relations A} →
                  {relations₂ : Module.Relations A} →
                    {solution₁ : relations₁.Solution M₁} →
                      {solution₂ : relations₂.Solution M₂} →
                        solution₁.IsPresentation →
                          solution₂.IsPresentation → (solution₁.tensor solution₂).IsPresentationCore
-- Mathlib.Analysis.Complex.Norm
Complex.norm_of_nonneg : ∀ {r : ℝ}, 0 ≤ r → ‖↑r‖ = r
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inl_fst_f_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : K.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f i) h) =
    h
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.collectLetValue : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → Lean.FVarIdHashSet → Lean.FVarIdHashSet
-- Mathlib.Topology.Order.OrderClosed
OrderClosedTopology.to_t2Space : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] [t : OrderClosedTopology α], T2Space α
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.annotateBool : Lean.Name → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Batteries.Data.PairingHeap
/-- Amortized `O(log n)`. Removes the smallest element from the heap, or `none` if the heap is empty.
 -/
Batteries.PairingHeap.tail? : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le → Option (Batteries.PairingHeap α le)
-- Mathlib.Analysis.Calculus.LHopital
/-- **L'Hôpital's rule** for approaching a real, `HasDerivAt` version  -/
HasDerivAt.lhopital_zero_nhds : ∀ {a : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in nhds a, HasDerivAt f (f' x) x) →
    (∀ᶠ (x : ℝ) in nhds a, HasDerivAt g (g' x) x) →
      (∀ᶠ (x : ℝ) in nhds a, g' x ≠ 0) →
        Filter.Tendsto f (nhds a) (nhds 0) →
          Filter.Tendsto g (nhds a) (nhds 0) →
            Filter.Tendsto (fun x => f' x / g' x) (nhds a) l → Filter.Tendsto (fun x => f x / g x) (nhdsWithin a {a}ᶜ) l
-- Mathlib.Probability.BrownianMotion.Basic
/-- **Weak Markov property**: If `B` is a pre-Brownian motion, then
`t ↦ B (t₀ + t) - B t₀` is a pre-Brownian motion which is independent from `(B t, t ≤ t₀)`.
This is the proof that it is pre-Brownian,
see `IsPreBrownianReal.indepFun_shift` for independence.  -/
ProbabilityTheory.IsPreBrownianReal.shift : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P →
    ∀ (t₀ : NNReal), ProbabilityTheory.IsPreBrownianReal (fun t ω => B (t₀ + t) ω - B t₀ ω) P
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
_private.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric.0.termσₙ : Lean.ParserDescr
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.cmpLT.trans_r : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α},
  RBTree.RBNode.cmpLT cmp x y →
    ∀ {a : RBTree.RBNode α},
      RBTree.RBNode.All (fun x_1 => RBTree.RBNode.cmpLT cmp x_1 x) a →
        RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp x y) a
-- Mathlib.Topology.ContinuousOn
ContinuousOn.congr_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s s₁ : Set α},
  ContinuousOn f s → Set.EqOn g f s₁ → s₁ ⊆ s → ContinuousOn g s₁
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.linearEquivFunOnFintype_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι] (a : Π₀ (i : ι), M i) (i : ι),
  DFinsupp.linearEquivFunOnFintype a i = a i
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.editCancellationTask : Lean.Server.RequestCancellationToken → Lean.Server.ServerTask Unit
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Use `snd_eq_support_getElem_one` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.support_getElem_one : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : 1 < p.support.length), p.support[1] = p.snd