mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Lemmas
USize.toUSize_toUInt32 : ∀ (n : USize), n.toUInt32.toUSize = n % 4294967296
-- Mathlib.Tactic.Convert
/-- Internal elaborator for `Convert.CheapConfig`: use `Convert.elabConfig` instead.  -/
Convert.elabCheapConfig : Lean.Syntax → optParam Convert.CheapConfig { } → optParam Bool true → Lean.Elab.Tactic.TacticM Convert.CheapConfig
-- Mathlib.Computability.NFA
NFA.evalFrom_iUnion : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {ι : Sort u_1} (s : ι → Set σ) (x : List α),
  M.evalFrom (⋃ i, s i) x = ⋃ i, M.evalFrom (s i) x
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the number of elements contained in the given closed range.
 -/
Std.Rcc.size : {α : Type u} → [Std.Rxc.HasSize α] → Std.Rcc α → ℕ
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.lift.eq_1 : ∀ {α : Type u_3} {M : Type u_4} [inst : AddMonoid M] (f : α → M) {rels : FreeAddMonoid α → FreeAddMonoid α → Prop}
  (h : ∀ (a b : FreeAddMonoid α), rels a b → (FreeAddMonoid.lift f) a = (FreeAddMonoid.lift f) b),
  PresentedAddMonoid.lift f h = (addConGen rels).lift (FreeAddMonoid.lift f) ⋯
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The inf of a set of orthogonal subspaces equals the subspace orthogonal to the sup.  -/
Submodule.sInf_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (s : Set (Submodule 𝕜 E)), ⨅ K ∈ s, Kᗮ = (sSup s)ᗮ
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
_private.Mathlib.RingTheory.SimpleModule.WedderburnArtin.0.isSemiprimaryRing_mulOpposite_iff : {R : Type u} → [inst : Ring R] → ProofWanted (IsSemiprimaryRing Rᵐᵒᵖ ↔ IsSemiprimaryRing R)
-- Init.Data.Range.Polymorphic.UInt
USize.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite USize
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_eq_cfcₙL : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} {f : R → R}
  (ha : p a) (hf : ContinuousOn f (quasispectrum R a)) (hf0 : f 0 = 0),
  cfcₙ f a = (cfcₙL ha) { toFun := (quasispectrum R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }
-- Batteries.Tactic.GeneralizeProofs
/-- Finds a proof of `prop` by looking at `propToFVar` and `propToProof`.
 -/
Batteries.Tactic.GeneralizeProofs.MAbs.findProof? : Lean.Expr → Batteries.Tactic.GeneralizeProofs.MAbs (Option Lean.Expr)
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.representableBy_homEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x : F.obj (Opposite.op X)} (h : F.IsRepresentedBy x) {Y : C} (f : Y ⟶ X),
  h.representableBy.homEquiv f = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) x
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.rid_tmul : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R S A] (r : R) (a : A),
  (Bialgebra.TensorProduct.rid R S A) (a ⊗ₜ[R] r) = r • a
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.le_withBotDegree : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ},
  d ∈ f.support → m.toWithBotSyn ↑d ≤ m.toWithBotSyn (m.withBotDegree f)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- In a group with zero, an existential over a unit can be rewritten in terms of `Units.mk0`.  -/
Units.exists0 : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {p : G₀ˣ → Prop}, (∃ g, p g) ↔ ∃ g, ∃ (hg : g ≠ 0), p (Units.mk0 g hg)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.irrelevant_eq_span : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜], (HomogeneousIdeal.irrelevant 𝒜).toIdeal = Ideal.span (⋃ i, ⋃ (_ : i > 0), ↑(𝒜 i))
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (toContinuousOrderHom : α →Co β)
  (exists_map_eq_of_map_le' :
    ∀ ⦃a : α⦄ ⦃b : β⦄, toContinuousOrderHom.toFun a ≤ b → ∃ c, a ≤ c ∧ toContinuousOrderHom.toFun c = b)
  (toContinuousOrderHom_1 : α →Co β)
  (exists_map_eq_of_map_le'_1 :
    ∀ ⦃a : α⦄ ⦃b : β⦄, toContinuousOrderHom_1.toFun a ≤ b → ∃ c, a ≤ c ∧ toContinuousOrderHom_1.toFun c = b),
  ({ toContinuousOrderHom := toContinuousOrderHom, exists_map_eq_of_map_le' := exists_map_eq_of_map_le' } =
      { toContinuousOrderHom := toContinuousOrderHom_1, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 }) =
    (toContinuousOrderHom = toContinuousOrderHom_1)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGE?ₘ'.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    [inst : Ord α] →
      (k : α) →
        (motive : Option ((a : α) × β a) → Std.DTreeMap.Internal.Impl.ExplorationStep α β (compare k) → Sort u_3) →
          (x : Option ((a : α) × β a)) →
            (x_1 : Std.DTreeMap.Internal.Impl.ExplorationStep α β (compare k)) →
              ((x : Option ((a : α) × β a)) →
                  (k' : α) →
                    (a : compare k k' = Ordering.lt) →
                      (v : β k') →
                        (a_1 : List ((a : α) × β a)) →
                          motive x (Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_1)) →
                ((base : Option ((a : α) × β a)) →
                    (a : List ((a : α) × β a)) →
                      (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
                        (r : List ((a : α) × β a)) →
                          motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a c r)) →
                  ((base : Option ((a : α) × β a)) →
                      (a : List ((a : α) × β a)) →
                        (a_1 : α) →
                          (a_2 : compare k a_1 = Ordering.gt) →
                            (a_3 : β a_1) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3)) →
                    motive x x_1
-- Init.Data.Iterators.Basic
/-- Converts a monadic iterator (`IterM Id β`) over `Id` into a pure iterator (`Iter β`).
 -/
Std.IterM.toIter : {α β : Type w} → Std.IterM Id β → Std.Iter β
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.coe_equivMapOfInjective_apply : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (S : Submonoid M) (f : M →* N)
  (hf : Function.Injective ⇑f) (x : ↥S), ↑((S.equivMapOfInjective f hf) x) = f ↑x
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
Measurable.untopD : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  [inst_3 : MeasurableSpace ι] [BorelSpace ι] {α : Type u_2} {mα : MeasurableSpace α} (d : ι) {f : α → WithTop ι},
  Measurable f → Measurable fun x => WithTop.untopD d (f x)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.comp_map₂ : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C)
  (G : CategoryTheory.StrictlyUnitaryLaxFunctor C D) {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  (F.comp G).map₂ η = G.map₂ (F.map₂ η)
-- Std.Async.TCP
/-- Tries to accept an incoming connection.
 -/
Std.Async.TCP.Socket.Server.tryAccept : Std.Async.TCP.Socket.Server → IO (Option Std.Async.TCP.Socket.Client)
-- Mathlib.RingTheory.Etale.StandardEtale
Algebra.IsStandardEtale.mk : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Nonempty (StandardEtalePresentation R S) → Algebra.IsStandardEtale R S
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.hom_ext_iff : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  {arrows : (j : J) → B ⟶ objs j} [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C}
  {g1 g2 : CategoryTheory.Limits.widePushout B objs arrows ⟶ X},
  g1 = g2 ↔
    (∀ (j : J),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι arrows j) g1 =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι arrows j) g2) ∧
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.head arrows) g1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.head arrows) g2
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.overMapUnitIso_inv_val_app_hom_apply : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D}
  {R : CategoryTheory.Sheaf K RingCat} {X Y : D} (f : X ⟶ Y) (x : (CategoryTheory.Over X)ᵒᵖ)
  (x_1 : ↑(((SheafOfModules.overMap R f).obj (SheafOfModules.unit (R.over Y))).val.obj x)),
  (ModuleCat.Hom.hom ((SheafOfModules.overMapUnitIso f).inv.val.app x)) x_1 = x_1
-- Mathlib.Algebra.Group.Basic
add_left_surjective : ∀ {G : Type u_3} [inst : AddGroup G] (a : G), Function.Surjective fun x => a + x
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Types.ListIterator.stepAsHetT_iterM.match_1.eq_2 : ∀ {β : Type u_1} (motive : List β → Sort u_2) (x : β) (xs : List β) (h_1 : Unit → motive [])
  (h_2 : (x : β) → (xs : List β) → motive (x :: xs)),
  (match x :: xs with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_2 x xs
-- Mathlib.Logic.Basic
Exists₂.imp : ∀ {α : Sort u_1} {β : α → Sort u_2} {p q : (a : α) → β a → Prop},
  (∀ (a : α) (b : β a), p a b → q a b) → (∃ a b, p a b) → ∃ a b, q a b
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.coe_refl : ∀ {A : Type u_1} [inst : Add A] [inst_1 : Mul A] [inst_2 : Star A], ⇑StarRingEquiv.refl = id
-- Init.Data.Int.Order
Int.sign_sign : ∀ {x : ℤ}, x.sign.sign = x.sign
-- Mathlib.Data.Multiset.Filter
Multiset.Nodup.filterMap : ∀ {α : Type u_1} {β : Type v} {s : Multiset α} (f : α → Option β),
  (∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a') → s.Nodup → (Multiset.filterMap f s).Nodup
-- Mathlib.Geometry.Euclidean.Inversion.Calculus
/-- Formula for the Fréchet derivative of `EuclideanGeometry.inversion c R`.  -/
EuclideanGeometry.hasFDerivAt_inversion : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {c x : F} {R : ℝ},
  x ≠ c → HasFDerivAt (EuclideanGeometry.inversion c R) ((R / dist x c) ^ 2 • ↑↑(ℝ ∙ (x - c))ᗮ.reflection) x
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.mul_zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F (x.mul CommRingCat.Colimits.Prequotient.zero) CommRingCat.Colimits.Prequotient.zero
-- Mathlib.Algebra.Algebra.Pi
/-- `Equiv.sumArrowEquivProdArrow` as an algebra equivalence.  -/
AlgEquiv.sumArrowEquivProdArrow : (α : Type u_1) →
  (β : Type u_2) →
    (R : Type u_3) →
      [inst : CommSemiring R] →
        (S : Type u_8) → [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (α ⊕ β → S) ≃ₐ[R] (α → S) × (β → S)
-- Mathlib.Data.EReal.Inv
EReal.div_nonpos_of_nonneg_of_nonpos : ∀ {a b : EReal}, 0 ≤ a → b ≤ 0 → a / b ≤ 0
-- Mathlib.NumberTheory.LucasLehmer
/-- If `2^p - 1` is prime then 3 is not a square mod `2^p - 1`.  -/
legendreSym_mersenne_three : ∀ {p : ℕ} [inst : Fact (Nat.Prime (mersenne p))], 3 ≤ p → Odd p → legendreSym (mersenne p) 3 = -1
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Finpartition.bind.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α] {a : α}
  (P : Finpartition a) (Q Q_1 : (i : α) → i ∈ P.parts → Finpartition i), Q = Q_1 → P.bind Q = P.bind Q_1
-- Lean.Meta.Match.Basic
Lean.Meta.Match.AltLHS.mk : Lean.Syntax → List Lean.LocalDecl → List Lean.Meta.Match.Pattern → Lean.Meta.Match.AltLHS
-- Mathlib.NumberTheory.LSeries.Convergence
LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeries.abscissaOfAbsConv f < ↑s.re → ∃ x < s.re, LSeriesSummable f ↑x
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Augment a `FieldSimp.NF M` object `l`, i.e. a list of pairs in `ℤ × M`, by prepending another
pair `p : ℤ × M`.  -/
Mathlib.Tactic.FieldSimp.NF.cons : {M : Type u_1} → ℤ × M → Mathlib.Tactic.FieldSimp.NF M → Mathlib.Tactic.FieldSimp.NF M
-- Std.Http.Protocol.H1.Error
/-- Generic error with message.
 -/
Std.Http.Protocol.H1.Error.other : String → Std.Http.Protocol.H1.Error
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.one_actLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (self : Bimod A B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one self.X) self.actLeft =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor self.X).hom
-- Mathlib.Algebra.Field.ULift
ULift.divisionSemiring : {α : Type u} → [DivisionSemiring α] → DivisionSemiring (ULift.{u_1, u} α)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If two sets coincide locally, except maybe at a point, then derivatives within these sets
coincide locally.  -/
mfderivWithin_eventually_congr_set' : ∀ {𝕜 : 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'} {x : M} {s t : Set M}
  (y : M), s =ᶠ[nhdsWithin x {y}ᶜ] t → ∀ᶠ (y : M) in nhds x, mfderiv[s] f y = mfderiv[t] f y
-- Mathlib.CategoryTheory.Galois.Basic
/-- Fiber functors are faithful.  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.instFaithfulFintypeCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F], F.Faithful
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.one_kroneckerTMul_one : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [inst : CommSemiring R]
  [inst_1 : AddCommMonoidWithOne α] [inst_2 : AddCommMonoidWithOne β] [inst_3 : Module R α] [inst_4 : Module R β]
  [inst_5 : DecidableEq m] [inst_6 : DecidableEq n], Matrix.kroneckerMap (TensorProduct.tmul R) 1 1 = 1
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.mk.inj : ∀ {A : Type u_1} {L : Type u_2} {inst : CommRing A} {inst_1 : LieRing L} {inst_2 : Module A L}
  {toSubmodule : Submodule A L}
  {lie_mem' : ∀ {a b : L}, a ∈ toSubmodule.carrier → b ∈ toSubmodule.carrier → ⁅a, b⁆ ∈ toSubmodule.carrier}
  {toSubmodule_1 : Submodule A L}
  {lie_mem'_1 : ∀ {a b : L}, a ∈ toSubmodule_1.carrier → b ∈ toSubmodule_1.carrier → ⁅a, b⁆ ∈ toSubmodule_1.carrier},
  { toSubmodule := toSubmodule, lie_mem' := lie_mem' } = { toSubmodule := toSubmodule_1, lie_mem' := lie_mem'_1 } →
    toSubmodule = toSubmodule_1
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.ppow_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R}, f.ppow 0 = ↑ArithmeticFunction.zeta
-- Mathlib.Algebra.GroupWithZero.Hom
coe_powMonoidWithZeroHom : ∀ {M₀ : Type u_6} [inst : CommMonoidWithZero M₀] {n : ℕ} (hn : n ≠ 0), ⇑(powMonoidWithZeroHom hn) = fun x => x ^ n
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderiv.eq_1 : ∀ {𝕜 : 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') (x : M),
  mfderiv% f x =
    if MDiffAt f x then fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (Set.range ↑I) (↑(extChartAt I x) x) else 0
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearRatUnits : {n : ℕ} → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.killCopies_def : ∀ {V : Type u_7} {W : Type u_8} (G : SimpleGraph V) (H : SimpleGraph W),
  G.killCopies H = if hH : H = ⊥ then G else G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})
-- Mathlib.Tactic.RenameBVar
/-- * `rename_bvar old → new` renames all bound variables named `old` to `new` in the target.
* `rename_bvar old → new at h` does the same in hypothesis `h`.

```lean
example (P : ℕ → ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m := by
  rename_bvar n → q at h -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
  rename_bvar m → n -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
  exact h -- Lean does not care about those bound variable names
```
Note: name clashes are resolved automatically.
 -/
Mathlib.Tactic.«tacticRename_bvar_→__» : Lean.ParserDescr
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_extendDomain : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (e : Equiv.Perm α) {p : β → Prop} [inst_4 : DecidablePred p] (f : α ≃ Subtype p),
  Equiv.Perm.sign (e.extendDomain f) = Equiv.Perm.sign e
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.of_mul_monic_right : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.Monic → (p * q).Monic → p.Monic
-- Mathlib.Analysis.Distribution.TemperateGrowth
MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [BorelSpace E] {μ : MeasureTheory.Measure E} [h : μ.IsAddHaarMeasure], μ.HasTemperateGrowth
-- Mathlib.Data.Nat.Digits.Defs
Nat.digitsAux_def : ∀ (b : ℕ) (h : 2 ≤ b) (n : ℕ), 0 < n → b.digitsAux h n = n % b :: b.digitsAux h (n / b)
-- Lean.Attributes
/-- If set, entries are not resorted on export and `getParam?` will fall back to a linear instead of
binary search inside an imported module's entries.
 -/
Lean.ParametricAttributeImpl.preserveOrder : {α : Type} → Lean.ParametricAttributeImpl α → Bool
-- Mathlib.Topology.Connected.Clopen
IsClopen.eq_univ : ∀ {α : Type u} [inst : TopologicalSpace α] [PreconnectedSpace α] {s : Set α}, IsClopen s → s.Nonempty → s = Set.univ
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.ofPrime_prime : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsDedekindDomain.HeightOneSpectrum.ofPrime ⋯ = v
-- Mathlib.Analysis.Calculus.TangentCone.Basic
tangentConeAt_mono : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : TopologicalSpace E] {s t : Set E}
  {x : E}, s ⊆ t → tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseNeg : Std.Internal.Parsec.ByteArray.Parser ℤ
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toProd_smul : ∀ {S : Type u_2} {R : Type u_3} {A : Type u_4} [inst : SMul S R] [inst_1 : SMul S A] (s : S) (x : Unitization R A),
  (s • x).toProd = s • x.toProd
-- Lean.Elab.DeclModifiers
Lean.Elab.instInhabitedComputeKind.default : Lean.Elab.ComputeKind
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.isIdempotentElem_rankOne_self : ∀ {𝕜 : Type u_4} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  {x : F}, ‖x‖ = 1 → IsIdempotentElem (((InnerProductSpace.rankOne 𝕜) x) x)
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- A vector space has dimension at most `1` if and only if there is a
single vector of which all vectors are multiples.  -/
rank_le_one_iff : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V], Module.rank K V ≤ 1 ↔ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
-- Mathlib.Data.PFun
PFun.monad : {α : Type u_1} → Monad (PFun α)
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContDiffAt.comp_contMDiffWithinAt : ∀ {𝕜 : 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] {F : Type u_6} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_7} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F']
  {n : WithTop ℕ∞} {g : F → F'} {f : M → F} {s : Set M} {x : M},
  ContDiffAt 𝕜 n g (f x) →
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F) n f s x →
      ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n (g ∘ f) s x
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.limitConeIsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections],
  CommMonCat.limitConeIsLimit F =
    CategoryTheory.liftedLimitIsLimit
      (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat)))
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.martingale_const : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] (ℱ : MeasureTheory.Filtration ι m0)
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (x : E),
  MeasureTheory.Martingale (fun x_1 x_2 => x) ℱ μ
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PartialMatch.c : Lean.Meta.LazyDiscrTree.PartialMatch → Lean.Meta.LazyDiscrTree.TrieIndex
-- Lean.Expr
_private.Lean.Expr.0.Lean.natAddFn : Lean.Expr
-- Lean.Compiler.InlineAttrs
Lean.Compiler.instHashableInlineAttributeKind : Hashable Lean.Compiler.InlineAttributeKind
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.subsingleton_iff : ∀ {R : Type u_6} {M : Type u_8} {M' : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (S : Submonoid R) (g : M →ₗ[R] M') [IsLocalizedModule S g],
  Subsingleton M' ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
-- Mathlib.Order.Category.Preord
Preord.of.injEq : ∀ (carrier : Type u_1) [str : Preorder carrier] (carrier_1 : Type u_1) (str_1 : Preorder carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Topology.Instances.NNReal.Lemmas
/-- An antitone, bounded below sequence `f : ℕ → ℝ` has a finite limit.  -/
Real.tendsto_of_bddBelow_antitone : ∀ {f : ℕ → ℝ}, BddBelow (Set.range f) → Antitone f → ∃ r, Filter.Tendsto f Filter.atTop (nhds r)
-- Init.Data.List.Sublist
List.IsInfix.map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) ⦃l₁ l₂ : List α⦄, l₁ <:+: l₂ → List.map f l₁ <:+: List.map f l₂