mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Expr
Lean.Expr.forallE.injEq : ∀ (binderName : Lean.Name) (binderType body : Lean.Expr) (binderInfo : Lean.BinderInfo) (binderName_1 : Lean.Name)
  (binderType_1 body_1 : Lean.Expr) (binderInfo_1 : Lean.BinderInfo),
  (Lean.Expr.forallE binderName binderType body binderInfo =
      Lean.Expr.forallE binderName_1 binderType_1 body_1 binderInfo_1) =
    (binderName = binderName_1 ∧ binderType = binderType_1 ∧ body = body_1 ∧ binderInfo = binderInfo_1)
-- Mathlib.Order.Filter.Basic
Filter.sInf_neBot_of_directed : ∀ {α : Type u} [Nonempty α] {s : Set (Filter α)}, DirectedOn (fun x1 x2 => x1 ≥ x2) s → ⊥ ∉ s → (sInf s).NeBot
-- Init.System.FilePath
System.FilePath.instDiv : Div System.FilePath
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_le : ∀ {a b : Int64}, a ≤ b → a.toNatClampNeg ≤ b.toNatClampNeg
-- Mathlib.Algebra.MonoidAlgebra.Division
/-- **Alias** of `AddMonoidAlgebra.coeff_modOf_of_not_exists_add`. -/
AddMonoidAlgebra.modOf_apply_of_not_exists_add : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (x : AddMonoidAlgebra k G) (g g' : G),
  (¬∃ d, g' = g + d) → (x.modOf g).coeff g' = x.coeff g'
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqResponseError.beq : {α : Type u_1} → [BEq α] → Lean.JsonRpc.ResponseError α → Lean.JsonRpc.ResponseError α → Bool
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_nat_mul_two_pi_sub : ∀ (x : ℂ) (n : ℕ), Complex.cos (↑n * (2 * ↑Real.pi) - x) = Complex.cos x
-- Mathlib.Topology.LocallyFinite
LocallyFinite.point_finite : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
  LocallyFinite f → ∀ (x : X), {b | x ∈ f b}.Finite
-- Mathlib.RingTheory.Coprime.Lemmas
Rat.isCoprime_num_den : ∀ (x : ℚ), IsCoprime x.num ↑x.den
-- Lean.Elab.Level
Lean.Elab.Level.State.mk.inj : ∀ {ngen : Lean.NameGenerator} {mctx : Lean.MetavarContext} {levelNames : List Lean.Name} {ngen_1 : Lean.NameGenerator}
  {mctx_1 : Lean.MetavarContext} {levelNames_1 : List Lean.Name},
  { ngen := ngen, mctx := mctx, levelNames := levelNames } =
      { ngen := ngen_1, mctx := mctx_1, levelNames := levelNames_1 } →
    ngen = ngen_1 ∧ mctx = mctx_1 ∧ levelNames = levelNames_1
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The first projection from the chosen pullback along `g` of `f` to the domain of `f`.  -/
CategoryTheory.ChosenPullbacksAlong.fst : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} →
      (f : Y ⟶ X) →
        (g : Z ⟶ X) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong g] → CategoryTheory.ChosenPullbacksAlong.pullbackObj f g ⟶ Y
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.hasPointwiseRightKanExtension_of_hasPointwiseLeftDerivedFunctor : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [F.HasPointwiseLeftDerivedFunctor W] [L.IsLocalization W], L.HasPointwiseRightKanExtension F
-- Mathlib.Order.OmegaCompletePartialOrder
_private.Mathlib.Order.OmegaCompletePartialOrder.0.OmegaCompletePartialOrder.Chain.pair.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((x : ℕ) → (x = 0 → False) → motive x) → motive x
-- Mathlib.Algebra.Group.Basic
add_add_add_comm : ∀ {G : Type u_3} [inst : AddCommSemigroup G] (a b c d : G), a + b + (c + d) = a + c + (b + d)
-- Mathlib.Data.List.Sort
List.mergeSort_eq_insertionSort : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [Std.Total r] [IsTrans α r] [Std.Antisymm r] (l : List α),
  (l.mergeSort fun x1 x2 => decide (r x1 x2)) = List.insertionSort r l
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Types.instReflectsColimitsOfSizeForgetTypeFun : CategoryTheory.Limits.ReflectsColimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (CategoryTheory.forget (Type u))
-- Mathlib.LinearAlgebra.CliffordAlgebra.Star
CliffordAlgebra.instStarRing : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → StarRing (CliffordAlgebra Q)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Operations.0.SimpleGraph.Walk.drop.match_1.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → ℕ → Sort u_2) (x : ℕ)
  (h_1 : (x : ℕ) → motive u SimpleGraph.Walk.nil x) (h_2 : (v : V) → (p : G.Walk u v) → motive v p 0)
  (h_3 : (v v_1 : V) → (h : G.Adj u v_1) → (q : G.Walk v_1 v) → (n : ℕ) → motive v (SimpleGraph.Walk.cons h q) n.succ),
  (match u, SimpleGraph.Walk.nil, x with
    | .(u), SimpleGraph.Walk.nil, x => h_1 x
    | v, p, 0 => h_2 v p
    | v, SimpleGraph.Walk.cons h q, n.succ => h_3 v v_1 h q n) =
    h_1 x
-- Init.Internal.Order.Basic
Lean.Order.fun_sup_eq : ∀ {α : Sort u} {β : α → Sort v} [inst : (x : α) → Lean.Order.CompleteLattice (β x)] (c : ((x : α) → β x) → Prop),
  Lean.Order.fun_sup c = Lean.Order.CompleteLattice.sup c
-- Mathlib.Algebra.Module.Presentation.Differentials
Algebra.Presentation.differentialsRelations_R : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ), pres.differentialsRelations.R = σ
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
AddMonoidAlgebra.instIsCocomm : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] {X : Type u_3} [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] [Coalgebra.IsCocomm R A], Coalgebra.IsCocomm R (AddMonoidAlgebra A X)
-- Init.Core
Nat.succ.inj : ∀ {m n : ℕ}, m.succ = n.succ → m = n
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.ext : ∀ {X : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  {x y : e₀₁.CompStruct e₁₂ e₀₂}, x.simplex = y.simplex → x = y
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentationCore.postcomp_desc : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (self : solution.IsPresentationCore) {N : Type w'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N), solution.postcomp (self.desc s) = s
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_updateBucket_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option (β a) → Option (β a)},
      Std.DHashMap.Internal.IsHashSelf
        (Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a (Std.DHashMap.Internal.AssocList.alter a f))
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The homology data for the short complexes given by the differentials
of a spectral sequence attached to a spectral object in an abelian category.  -/
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    [inst_3 : X.HasSpectralSequence data] →
                      (r r' : ℤ) →
                        (hrr' : r + 1 = r') →
                          (hr : r₀ ≤ r) →
                            (pq pq' pq'' : κ) →
                              (c r).prev pq' = pq →
                                (c r).next pq' = pq'' →
                                  (i₀' i₀ i₁ i₂ i₃ i₃' : ι) →
                                    i₀' = data.i₀ r' pq' ⋯ →
                                      i₀ = data.i₀ r pq' ⋯ →
                                        i₁ = data.i₁ pq' →
                                          i₂ = data.i₂ pq' →
                                            i₃ = data.i₃ r pq' ⋯ →
                                              i₃' = data.i₃ r' pq' ⋯ →
                                                (n₀ n₁ n₂ : ℤ) →
                                                  n₁ = data.deg pq' →
                                                    autoParam (n₀ + 1 = n₁)
                                                        CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_1 →
                                                      autoParam (n₁ + 1 = n₂)
                                                          CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_3 →
                                                        (((X.spectralSequence data).page r hr).sc' pq pq'
                                                            pq'').HomologyData
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry.userName : Lean.Meta.SimpAll.Entry → Lean.Name
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaPairing_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (P Q : C × CategoryTheory.Functor C (Type v₁)) (α : P ⟶ Q)
  (β : (CategoryTheory.coyonedaPairing C).obj P),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.coyonedaPairing C).map α)) β =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map α.1.op) (CategoryTheory.CategoryStruct.comp β α.2)
-- Init.Data.String.Defs
List.utf8Encode_eq_empty : ∀ {l : List Char}, l.utf8Encode = ByteArray.empty ↔ l = []
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.StronglyAdapted.isStoppingTime_lowerCrossingTime : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.StronglyAdapted ℱ f →
    MeasureTheory.IsStoppingTime ℱ fun ω => ↑(MeasureTheory.lowerCrossingTime a b f N n ω)
-- Mathlib.LinearAlgebra.Prod
LinearMap.snd_comp_inl : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], LinearMap.snd R M M₂ ∘ₗ LinearMap.inl R M M₂ = 0
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A locally uniform limit on a set of functions which are continuous on this set is itself
continuous on this set.  -/
TendstoLocallyUniformlyOn.continuousOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι},
  TendstoLocallyUniformlyOn F f p s → (∃ᶠ (n : ι) in p, ContinuousOn (F n) s) → ContinuousOn f s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} {fallback : β a}, m.isEmpty = true → m.getD a fallback = fallback
-- Mathlib.LinearAlgebra.Span.Basic
/-- The product of two submodules is a submodule.  -/
Submodule.prod : {R : Type u_1} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          Submodule R M →
            {M' : Type u_8} →
              [inst_3 : AddCommMonoid M'] → [inst_4 : Module R M'] → Submodule R M' → Submodule R (M × M')
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
_private.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card.0.termN : Lean.ParserDescr
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.discreteTopology_of_toLocalization_surjective : ∀ {R : Type u} [inst : CommSemiring R],
  Function.Surjective ⇑(PrimeSpectrum.toPiLocalization R) → DiscreteTopology (PrimeSpectrum R)
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctorMapObj_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K}
  [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
  {f g : CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y k ⟶ A},
  (∀ (i : I) (j : J) (hij : p (i, j) = k),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) g) →
    f = g
-- Mathlib.Analysis.Complex.CanonicalDecomposition
_private.Mathlib.Analysis.Complex.CanonicalDecomposition.0.Complex.canonicalDecomposition_aux₃ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {f : ℂ → E} {z : ℂ},
  0 < R →
    meromorphicOrderAt (∏ᶠ (c : ℂ), Complex.canonicalFactor R c ^ (MeromorphicOn.divisor f (Metric.ball 0 R)) c) z ≠ ⊤
-- Mathlib.Algebra.Lie.Loop
LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : CommRing A] [inst_4 : IsAddTorsionFree R] [inst_5 : Algebra A R] (Φ : LinearMap.BilinForm R L)
  (hΦ : Φ.IsSymm) (x y : LieAlgebra.loopAlgebra R A L),
  ((LieAlgebra.LoopAlgebra.twoCochainOfBilinear R A L Φ hΦ) x) y =
    (TrivialLieModule.equiv R (LieAlgebra.loopAlgebra R A L) R).symm
      (((LieAlgebra.LoopAlgebra.residuePairing R A L Φ) x) y)
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.inst : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] → (ψ : L →ₗ⁅R⁆ LieDerivation R K K) → LieAlgebra R (K ⋊⁅ψ⁆ L)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.inf_toNonUnitalSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (S T : NonUnitalSubalgebra R A),
  (S ⊓ T).toNonUnitalSubsemiring = S.toNonUnitalSubsemiring ⊓ T.toNonUnitalSubsemiring
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.const_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β],
  ContinuousMap.const α 0 = 0
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.functorProdFunctorEquiv_inverse : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C],
  (CategoryTheory.functorProdFunctorEquiv A B C).inverse = CategoryTheory.functorProdToProdFunctor A B C
-- Mathlib.Algebra.Group.Fin.Basic
Fin.addCommGroup : (n : ℕ) → [NeZero n] → AddCommGroup (Fin n)
-- Mathlib.Logic.Relation
Relation.TransGen.head' : ∀ {α : Type u_1} {r : α → α → Prop} {a b c : α}, r a b → Relation.ReflTransGen r b c → Relation.TransGen r a c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).maxKey? = some (t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k')
-- Mathlib.Analysis.Convex.Topology
/-- Convex hull of a finite set is compact.  -/
Set.Finite.isCompact_convexHull : ∀ {E : Type u_3} (𝕜 : Type u_4) [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderClosedTopology 𝕜] [CompactIccSpace 𝕜] [ContinuousAdd 𝕜] [inst_7 : AddCommGroup E]
  [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E},
  s.Finite → IsCompact ((convexHull 𝕜) s)
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_mul_natCast : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a k : ℕ}, (p * ↑a).coeff k = p.coeff k * ↑a
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_nsmul_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E} {n : ℕ}, ‖n • a‖₊ ≤ ↑n * ‖a‖₊
-- Init.Data.Function
/-- Transforms a function from pairs into an equivalent two-parameter function.

Examples:
* `Function.curry (fun (x, y) => x + y) 3 5 = 8`
* `Function.curry Prod.swap 3 "five" = ("five", 3)`
 -/
Function.curry : {α : Type u_1} → {β : Type u_2} → {φ : Sort u_3} → (α × β → φ) → α → β → φ
-- Init.Data.List.Lemmas
List.getElem?_replace : ∀ {α : Type u_1} [inst : BEq α] {a b : α} [inst_1 : LawfulBEq α] {l : List α} {i : ℕ},
  (l.replace a b)[i]? = if (l[i]? == some a) = true then if a ∈ List.take i l then some a else some b else l[i]?
-- Lean.Parser.Term
Lean.Parser.Term.waitIfTypeContainsMVar.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
UniqueMDiffOn.eq : ∀ {𝕜 : 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 : Set M}
  {f' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
  UniqueMDiff[s] → x ∈ s → HasMFDerivAt[s] f x f' → HasMFDerivAt[s] f x f₁' → f' = f₁'
-- Std.Internal.Parsec.String
/-- Parse a hex digit `0-9`, `a-f`, or `A-F` as a `Char`.
 -/
Std.Internal.Parsec.String.hexDigit : Std.Internal.Parsec.String.Parser Char
-- Mathlib.Topology.UniformSpace.HeineCantor
/-- A family of functions `α → β → γ` tends uniformly to its value at `x` if `α` is locally compact,
`β` is compact and `f` is continuous on `U × (univ : Set β)` for some neighborhood `U` of `x`.  -/
ContinuousOn.tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β] [LocallyCompactSpace α]
  [CompactSpace β] [inst_4 : UniformSpace γ] {f : α → β → γ} {x : α} {U : Set α},
  U ∈ nhds x → ContinuousOn (↿f) (U ×ˢ Set.univ) → TendstoUniformly f (f x) (nhds x)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.id : Lean.Syntax → Lean.Name → Bool → Lean.LocalContext → Option Lean.Expr → Lean.Elab.CompletionInfo
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_sub`. -/
SkewMonoidAlgebra.toFinsupp_sub : ∀ {k : Type u_1} {G : Type u_2} [inst : AddGroup k] (a b : SkewMonoidAlgebra k G), (a - b).coeff = a.coeff - b.coeff
-- Init.Data.String.PosRaw
String.Pos.Raw.offsetBy_assoc : ∀ {p q r : String.Pos.Raw}, (p.offsetBy q).offsetBy r = p.offsetBy (q.offsetBy r)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.LocallyDirected.mk : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X} →
      [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] →
        (trans : {i j : 𝒰.I₀} → (i ⟶ j) → (𝒰.X i ⟶ 𝒰.X j)) →
          autoParam
              (∀ (i : 𝒰.I₀), trans (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (𝒰.X i))
              AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_id._autoParam →
            autoParam
                (∀ {i j k : 𝒰.I₀} (hij : i ⟶ j) (hjk : j ⟶ k),
                  trans (CategoryTheory.CategoryStruct.comp hij hjk) =
                    CategoryTheory.CategoryStruct.comp (trans hij) (trans hjk))
                AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_comp._autoParam →
              (w :
                  autoParam
                    (∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (trans hij) (𝒰.f j) = 𝒰.f i)
                    AlgebraicGeometry.Scheme.Cover.LocallyDirected.w._autoParam) →
                (∀ {i j : 𝒰.I₀} (x : ↥(CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))),
                    ∃ k hki hkj y, (CategoryTheory.Limits.pullback.lift (trans hki) (trans hkj) ⋯) y = x) →
                  autoParam (∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (trans hij))
                      AlgebraicGeometry.Scheme.Cover.LocallyDirected.property_trans._autoParam →
                    𝒰.LocallyDirected
-- Plausible.Sampleable
Plausible.SampleableExt.shrink : {α : Sort u} → [self : Plausible.SampleableExt α] → Plausible.Shrinkable (Plausible.SampleableExt.proxy α)
-- Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
/-- If `S` is finite as a module over `R` and finitely presented as an algebra over `R`, then
it is finitely presented as a module over `R`.  -/
Module.FinitePresentation.of_finite_of_finitePresentation : ∀ (R : Type u) (S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Finite R S]
  [Algebra.FinitePresentation R S], Module.FinitePresentation R S
-- Mathlib.NumberTheory.Dioph
/-- Deleting the first component preserves the Diophantine property.  -/
Dioph.vec_ex1_dioph : ∀ (n : ℕ) {S : Set (Vector3 ℕ n.succ)}, Dioph S → Dioph {v | ∃ x, Vector3.cons x v ∈ S}
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqFnBody : BEq Lean.IR.FnBody
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Std.Data.ExtDHashMap.Lemmas
Quotient.mk.eq_1 : ∀ {α : Sort u} (s : Setoid α) (a : α), ⟦a⟧ = Quot.mk (⇑s) a
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.range_subtype : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.subtype.range = H
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_lt_top_iff : ∀ {a : ENNReal} {n : ℕ}, a ^ n < ⊤ ↔ a < ⊤ ∨ n = 0
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.norm_σ : ∀ (g : GL (Fin 2) ℝ) (z : ℂ), ‖(UpperHalfPlane.σ g) z‖ = ‖z‖
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.isAnisotropic_of_isValuedIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  (S : Type u_5) [inst_6 : CommRing S] [inst_7 : LinearOrder S] [IsStrictOrderedRing S] [inst_9 : Algebra S R]
  [FaithfulSMul S R] [P.IsValuedIn S], P.IsAnisotropic
-- Mathlib.Data.Finset.Functor
Finset.fmap_def : ∀ {α β : Type u} [inst : (P : Prop) → Decidable P] {s : Finset α} (f : α → β), f <$> s = Finset.image f s
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
PowerBasis.equivAdjoinSimple_symm_gen : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (pb : PowerBasis K L),
  pb.equivAdjoinSimple.symm pb.gen = IntermediateField.AdjoinSimple.gen K pb.gen
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `r : R` is equal to 1 if and only if `r ∈ vᶜ`.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff_mem_primeCompl : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  v.intValuation r = 1 ↔ r ∈ v.asIdeal.primeCompl
-- Mathlib.Algebra.Regular.SMul
/-- Left-regular multiplication on `R` is equivalent to `R`-regularity of `R` itself.  -/
isLeftRegular_iff : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsLeftRegular a ↔ IsSMulRegular R a