mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Quotient
/-- If `L' : Quotient homRel ⥤ D` satisfies the strict universal property of the
localization, then `Quotient.functor homRel ⋙ L'` also satisfies it.  -/
HomRel.FactorsThroughLocalization.strictUniversalPropertyFixedTarget : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {homRel : HomRel C} →
          {W : CategoryTheory.MorphismProperty C} →
            homRel.FactorsThroughLocalization W →
              {W' : CategoryTheory.MorphismProperty (CategoryTheory.Quotient homRel)} →
                W = W'.inverseImage (CategoryTheory.Quotient.functor homRel) →
                  {E : Type u_3} →
                    [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                      (L' : CategoryTheory.Functor (CategoryTheory.Quotient homRel) D) →
                        CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L' W' E →
                          CategoryTheory.Localization.StrictUniversalPropertyFixedTarget
                            ((CategoryTheory.Quotient.functor homRel).comp L') W E
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.LocallyOfFinitePresentation f],
  AlgebraicGeometry.LocallyOfFinitePresentation (f ∣_ V)
-- Mathlib.RingTheory.IsGaloisGroup.Basic
IsGaloisGroup.instSubtypeMemSubgroupSubalgebraSubalgebra : ∀ (G : Type u_1) [inst : Group G] (H : Subgroup G) (R : Type u_2) (S : Type u_3) [inst_1 : CommRing R]
  [inst_2 : CommRing S] [inst_3 : Algebra R S] [inst_4 : MulSemiringAction G S] [hGKL : IsGaloisGroup G R S],
  IsGaloisGroup (↥H) (↥(FixedPoints.subalgebra R S ↥H)) S
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
/-- A function `f` is integrable with respect to a countable sum of
Dirac masses `Measure.sum (fun i ↦ (c i) • Measure.dirac (x i))` if and only if
the sequence `fun i ↦ (c i).toReal * ‖f (x i)‖` is summable.  -/
MeasureTheory.integrable_sum_dirac_iff : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [Countable ι] {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {f : X → E} [MeasurableSingletonClass X] {x : ι → X} {c : ι → ENNReal},
  (∀ (i : ι), c i ≠ ⊤) →
    (MeasureTheory.Integrable f (MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (x i)) ↔
      Summable fun i => (c i).toReal * ‖f (x i)‖)
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.multispanShape.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1)
  (Z Z_1 : C) (e_Z : Z = Z_1) [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C],
  CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z =
    CategoryTheory.OrthogonalReflection.D₂.multispanShape W_1 Z_1
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
/-- The fpqc topology on the category of schemes is topology generated by the fpqc precoverage.  -/
AlgebraicGeometry.Scheme.fpqcTopology : CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.instLTLex : {ι : Type u_1} →
  {α : ι → Type u_2} → [inst : (i : ι) → Zero (α i)] → [LT ι] → [(i : ι) → LT (α i)] → LT (Lex (Π₀ (i : ι), α i))
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.ext_iff : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst : Group G} {inst_1 : MulAction G X}
  {x y : DiscreteTiling.Protoset G X ιₚ}, x = y ↔ ↑x = ↑y
-- Init.Data.UInt.Lemmas
USize.toFin_ofFin : ∀ (n : Fin USize.size), (USize.ofFin n).toFin = n
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.default_Γ' : default = Turing.PartrecToTM2.Γ'.consₗ
-- Mathlib.Order.Filter.Subsingleton
/-- We say that a filter is a *subsingleton* if there exists a subsingleton set
that belongs to the filter.  -/
Filter.Subsingleton : {α : Type u_1} → Filter α → Prop
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.instCoeOutLinearEquivId : {R : Type u_2} →
  {M₁ : Type u_5} →
    {M₂ : Type u_6} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} →
                        {Q₂ : QuadraticMap R M₂ N} → CoeOut (Q₁.IsometryEquiv Q₂) (M₁ ≃ₗ[R] M₂)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- The composition of a continuous function and an ae strongly measurable function is ae strongly
measurable.  -/
Continuous.comp_aestronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : β → γ} {f : α → β},
  Continuous g → MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => g (f x)) μ
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.trans_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : AddCommGroup V₃]
  [inst_4 : Module k V₁] [inst_5 : Module k V₂] [inst_6 : Module k V₃] [inst_7 : AddTorsor V₁ P₁]
  [inst_8 : AddTorsor V₂ P₂] [inst_9 : AddTorsor V₃ P₃] (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) (p : P₁),
  (e.trans e') p = e' (e p)
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instDecidableLeOffset : {x y : Std.Time.Millisecond.Offset} → Decidable (x ≤ y)
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_ssubset_Iic_self : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iio a ⊂ Set.Iic a
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by inversion.  -/
ContinuousMonoidHom.inv : (E : Type u_6) → [inst : CommGroup E] → [inst_1 : TopologicalSpace E] → [IsTopologicalGroup E] → E →ₜ* E
-- Mathlib.Topology.UniformSpace.Compact
Filter.HasBasis.lebesgue_number_lemma_nhdsWithin' : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {ι' : Sort u_2} {p : ι' → Prop} {V : ι' → Set (α × α)}
  {U : (x : α) → x ∈ K → Set α},
  (uniformity α).HasBasis p V →
    IsCompact K →
      (∀ (x : α) (hx : x ∈ K), U x hx ∈ nhdsWithin x K) →
        ∃ i, p i ∧ ∀ x ∈ K, ∃ y, UniformSpace.ball x (V i) ∩ K ⊆ U ↑y ⋯
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_same : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {f : α →₀ M}, (Finsupp.erase a f) a = 0
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.ofHom₂_hom_apply_hom : ∀ {R : Type u_1} [inst : CommRing R] {M N P : ModuleCat R} (f : ↑M →ₗ[R] ↑N →ₗ[R] ↑P) (x : ↑M),
  ModuleCat.Hom.hom ((ModuleCat.Hom.hom (ModuleCat.ofHom₂ f)) x) = f x
-- Mathlib.Order.Filter.Pointwise
Filter.smul_eq_bot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g : Filter β}, f • g = ⊥ ↔ f = ⊥ ∨ g = ⊥
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.exists_notMem_isStandardOpenImmersion : ∀ {R : Type u_1} {S : Type u_2} {inst : CommSemiring R} {inst_1 : CommSemiring S} {inst_2 : Algebra R S}
  [self : Algebra.IsLocalIso R S] (q : Ideal S) [q.IsPrime],
  ∃ g ∉ q, Algebra.IsStandardOpenImmersion R (Localization.Away g)
-- Lean.Parser.Term.Doc
/-- Information about how to spell a certain notation for an identifier in declaration names.  -/
Lean.Parser.Term.Doc.RecommendedSpelling : Type
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.middle_assoc_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.actLeft B.X)
      (CategoryTheory.CategoryStruct.comp self.actRight h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X self.X B.X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.actRight)
        (CategoryTheory.CategoryStruct.comp self.actLeft h))
-- Mathlib.Data.TypeVec
TypeVec.toSubtype.eq_1 : ∀ (n : ℕ) (x_5 : TypeVec.{u} n.succ) (p : x_5.Arrow (TypeVec.repeat n.succ Prop)) (i : Fin2 n)
  (x_6 : { x // TypeVec.ofRepeat (p i.fs x) }),
  TypeVec.toSubtype p i.fs x_6 = TypeVec.toSubtype (TypeVec.dropFun p) i x_6
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filterWithPostcondition_eq_toIter_filterMapWithPostcondition_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [inst_1 : Monad m]
  {f : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)},
  Std.Iter.filterWithPostcondition f it = Std.IterM.filterWithPostcondition f it.toIterM
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ico_Ioi_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ico (Filter.principal (Set.Ioi a)) (Filter.principal (Set.Ioi a))
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.complexEmbedding_apply : ∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ) (u : (NumberField.RingOfIntegers K)ˣ),
  ↑((NumberField.Units.complexEmbedding φ) u) = φ ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insert!_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {v : β k}, (compare (Std.DTreeMap.Internal.Impl.insert! k v t).minKey! k).isLE = true
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instForInOfTransCmpOfLawfulMonad : {α : Type u} →
  {cmp : α → α → Ordering} →
    {m : Type w → Type w₂} → [Std.TransCmp cmp] → [inst : Monad m] → [LawfulMonad m] → ForIn m (Std.ExtTreeSet α cmp) α
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.restrict.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : AddSubmonoid M}
  {N' : AddSubmonoid N} {f : M →+ N} (h : Set.MapsTo ⇑f ↑M' ↑N'),
  AddMonoidHom.restrict h = (f.domRestrict M').codRestrict N' ⋯
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₁ b) ↔ ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b
-- Init.Data.Array.FinRange
Array.finRange_zero : Array.finRange 0 = #[]
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_desc_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
  (hc : ∀ (j : ι), ∃ i, c.Rel i j) (i j : ι) {Z : C} (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j)
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homotopyCofiber.desc φ α hα).f j) h) =
    CategoryTheory.CategoryStruct.comp (hα.hom i j) h
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instToMessageDataSuggestionText : Lean.ToMessageData Lean.Meta.Tactic.TryThis.SuggestionText
-- Init.Data.String.Iterator
instReprIterator : Repr String.Legacy.Iterator
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.chainsIso₃.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.chainsIso₃ A =
    (Finsupp.domLCongr
        ((Fin.consEquiv fun i => G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x => G)))).toModuleIso
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_maxKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey?.isSome = true ↔ t.isEmpty = false
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.Pi.cons.congr_simp : ∀ {α : Type u_1} {δ : α → Sort v} {inst : DecidableEq α} [inst_1 : DecidableEq α] (s : Finset α) (a : α) (b b_1 : δ a),
  b = b_1 →
    ∀ (f f_1 : (a : α) → a ∈ s → δ a),
      f = f_1 → ∀ (a' : α) (h : a' ∈ insert a s), Finset.Pi.cons s a b f a' h = Finset.Pi.cons s a b_1 f_1 a' ⋯
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.finInsertNth : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {X : Fin (n + 1) → Type u_5}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)] (i : Fin (n + 1)) {f : α → X i}
  {g : α → (j : Fin n) → X (i.succAbove j)} {a : α} {s : Set α},
  ContinuousWithinAt f s a → ContinuousWithinAt g s a → ContinuousWithinAt (fun a => i.insertNth (f a) (g a)) s a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.pow.injEq : ∀ (a : Lean.Grind.CommRing.Expr) (k : ℕ) (a_1 : Lean.Grind.CommRing.Expr) (k_1 : ℕ),
  (a.pow k = a_1.pow k_1) = (a = a_1 ∧ k = k_1)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curryHomEquiv'_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.Closed X] (f : X ⟶ Y),
  CategoryTheory.MonoidalClosed.curryHomEquiv' f = CategoryTheory.MonoidalClosed.curry' f
-- Mathlib.Order.Interval.Basic
Interval.instCoeNonemptyInterval : {α : Type u_1} → [inst : LE α] → Coe (NonemptyInterval α) (Interval α)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (μ : CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPost F)
  (X X_1 X_2 : C),
  (((CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap μ).app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((μ.app X).app X_1) (F.obj X_2))
      (CategoryTheory.CategoryStruct.comp ((μ.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X X_1)).app X_2)
        (F.map (CategoryTheory.MonoidalCategoryStruct.associator X X_1 X_2).hom))
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- If a `C^m` function `f : M → E`, where `M` is some manifold, takes values in the
sphere, then it restricts to a `C^m` function from `M` to the sphere.  -/
ContMDiff.codRestrict_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {m : WithTop ℕ∞} {F : Type u_2}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type u_3} [inst_4 : TopologicalSpace H]
  {I : ModelWithCorners ℝ F H} {M : Type u_4} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M]
  [IsManifold I m M] {n : ℕ} [inst_8 : Fact (Module.finrank ℝ E = n + 1)] {f : M → E},
  ContMDiff I (modelWithCornersSelf ℝ E) m f →
    ∀ (hf' : ∀ (x : M), f x ∈ Metric.sphere 0 1),
      ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) m (Set.codRestrict f (Metric.sphere 0 1) hf')
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.mulMap'_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (A B : Subalgebra R S), Function.Surjective ⇑(A.mulMap' B)
-- Init.Data.ByteArray.Lemmas
ByteArray.toList.loop.eq_1 : ∀ (bs : ByteArray) (i : ℕ) (r : List UInt8),
  ByteArray.toList.loop bs i r = if i < bs.size then ByteArray.toList.loop bs (i + 1) (bs.get! i :: r) else r.reverse
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.instEmptyCollection : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Std.Internal.IndexMultiMap α β)
-- Mathlib.LinearAlgebra.Dimension.Localization
IsBaseChange.rank_eq : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {T : Type uT}
  [inst_3 : CommRing T] [NoZeroDivisors T] [inst_5 : Algebra R T] [FaithfulSMul R T] {P : Type uM}
  [inst_7 : AddCommGroup P] [inst_8 : Module R P] [inst_9 : Module T P] [inst_10 : IsScalarTower R T P] {g : M →ₗ[R] P},
  IsBaseChange T g → Module.rank T P = Module.rank R M
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableAt_id : ∀ {𝕜 : 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] {x : M}, MDiffAt id x
-- Mathlib.Data.PNat.Basic
PNat.le_sub_one_of_lt : ∀ {a b : ℕ+}, a < b → a ≤ b - 1
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piLTLim.congr_simp : ∀ {ι : Type u_6} [inst : LinearOrder ι] {X : ι → Type u_7} {i : ι} (hi : Order.IsSuccPrelimit i),
  InverseSystem.piLTLim hi = InverseSystem.piLTLim hi
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_inj_of_len_eq : ∀ {b : ℕ},
  1 < b →
    ∀ {L1 L2 : List ℕ},
      L1.length = L2.length → (∀ l ∈ L1, l < b) → (∀ l ∈ L2, l < b) → Nat.ofDigits b L1 = Nat.ofDigits b L2 → L1 = L2
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_iff_comap_le : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H ≤ H
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C}
  {inst_1 : CategoryTheory.MonoidalCategory C} [self : W.IsMonoidal], W.IsMultiplicative
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- **Alias** of the forward direction of `hasSumUniformly_iff_tendstoUniformly`. -/
HasSumUniformly.tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α], HasSumUniformly f g → TendstoUniformly (fun x1 x2 => ∑ i ∈ x1, f i x2) g Filter.atTop
-- Mathlib.Topology.Maps.Basic
IsClosedMap.closure_image_subset : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f → ∀ (s : Set X), closure (f '' s) ⊆ f '' closure s
-- Mathlib.Algebra.Polynomial.CoeffMem
Polynomial.idealSpan_range_update_divByMonic : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : DecidableEq ι] {i j : ι},
  i ≠ j → ∀ (v : ι → Polynomial R), Ideal.span (Set.range (Function.update v j (v j %ₘ v i))) = Ideal.span (Set.range v)
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.hasProd_symmetricIoc_int_iff : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : ℤ → α} {a : α},
  HasProd f a (SummationFilter.symmetricIoc ℤ) ↔
    Filter.Tendsto (fun N => ∏ n ∈ Finset.Ioc (-↑N) ↑N, f n) Filter.atTop (nhds a)
-- Mathlib.Algebra.Star.Unitary
Unitary.instStarModuleSubtypeMemSubmonoidUnitary : ∀ {R : Type u_1} {A : Type u_2} [inst : Monoid R] [inst_1 : Monoid A] [inst_2 : MulAction R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : StarMul R] [inst_6 : StarMul A]
  [inst_7 : StarModule R A], StarModule ↥(unitary R) ↥(unitary A)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₃ = f.f₃.τ₁
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.pow_eq_prod_const : ∀ {M : Type u_4} [inst : CommMonoid M] (b : M) (n : ℕ), b ^ n = ∏ _k ∈ Finset.range n, b
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.map_mk₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : CategoryTheory.HasShift D M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0)
  (f : X ⟶ Y) (F : CategoryTheory.Functor C D) [inst_5 : F.CommShift M],
  (CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f).map F = CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (F.map f)
-- Init.Data.Order.Ord
Std.TransCmp.congr_left : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α}, cmp a b = Ordering.eq → cmp a c = cmp b c
-- Std.Http.Data.Headers.Value
Std.Http.Header.Value.mk.injEq : ∀ (value : String)
  (isValidHeaderValue :
    autoParam (Std.Http.Header.IsValidHeaderValue value) Std.Http.Header.Value.isValidHeaderValue._autoParam)
  (value_1 : String)
  (isValidHeaderValue_1 :
    autoParam (Std.Http.Header.IsValidHeaderValue value_1) Std.Http.Header.Value.isValidHeaderValue._autoParam),
  ({ value := value, isValidHeaderValue := isValidHeaderValue } =
      { value := value_1, isValidHeaderValue := isValidHeaderValue_1 }) =
    (value = value_1)
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `C ≤ f'`, then
`f` grows at least as fast as `C * x` on `D`, i.e., `C * (y - x) ≤ f y - f x` whenever `x, y ∈ D`,
`x ≤ y`.  -/
Convex.mul_sub_le_image_sub_of_le_deriv : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D →
        DifferentiableOn ℝ f (interior D) →
          ∀ {C : ℝ}, (∀ x ∈ interior D, C ≤ deriv f x) → ∀ x ∈ D, ∀ y ∈ D, x ≤ y → C * (y - x) ≤ f y - f x
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.k_self : ∀ (R : Type u_1) [inst : CommRing R] {c₁ c₂ c₃ : R},
  (QuaternionAlgebra.Basis.self R).k = { re := 0, imI := 0, imJ := 0, imK := 1 }
-- Mathlib.Topology.Separation.Hausdorff
/-- If a function `f` is

- injective on a compact set `s`;
- continuous at every point of this set;
- injective on a neighborhood of each point of this set,

then it is injective on a neighborhood of this set.  -/
Set.InjOn.exists_mem_nhdsSet : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {f : X → Y}
  {s : Set X},
  Set.InjOn f s →
    IsCompact s → (∀ x ∈ s, ContinuousAt f x) → (∀ x ∈ s, ∃ u ∈ nhds x, Set.InjOn f u) → ∃ t ∈ nhdsSet s, Set.InjOn f t
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- A weak rank function `h : A.PairingCore` is a function from the index type `h.ι`
to a partially ordered type which maps an ancestrality relation between
indices of the same dimension to a strict inequality.  -/
SSet.Subcomplex.PairingCore.WeakRankFunction : {X : SSet} → {A : X.Subcomplex} → A.PairingCore → (α : Type v) → [PartialOrder α] → Type (max u_1 v)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_min?_iff_isEmpty_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → (t.min?.isSome = true ↔ t.isEmpty = false)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instWeakEquivalenceI₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A)
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty]
  [(HomotopicalAlgebra.weakEquivalences C).ContainsIdentities], HomotopicalAlgebra.WeakEquivalence P.i₁
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.instFunctorObj : (P : PFunctor.{uA, uB}) → Functor ↑P
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instInhabitedSimpEntry.default : Lean.Meta.SimpEntry