mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Small.List
smallList : ∀ {α : Type v} [Small.{u, v} α], Small.{u, v} (List α)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_sup_ideal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (I J : Ideal A),
  ProjectiveSpectrum.zeroLocus 𝒜 ↑(I ⊔ J) = ProjectiveSpectrum.zeroLocus 𝒜 ↑I ∩ ProjectiveSpectrum.zeroLocus 𝒜 ↑J
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getUserGeneralizingFVarIds : Lean.Syntax → Lean.Elab.Tactic.TacticM (Array Lean.FVarId)
-- Mathlib.RingTheory.TensorProduct.Basic
LinearMap.mul'_tensor : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : SMulCommClass R A A]
  [inst_6 : SMulCommClass R B B] [inst_7 : IsScalarTower R A A] [inst_8 : IsScalarTower R B B],
  LinearMap.mul' R (TensorProduct R A B) =
    TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R B) ∘ₗ ↑(TensorProduct.tensorTensorTensorComm R A B A B)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_empty : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal), Metric.externalCoveringNumber ε ∅ = 0
-- Init.Data.String.Basic
String.Pos.ofSlice_startPos : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}, String.Pos.ofSlice (s.slice p₀ p₁ h).startPos = p₀
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits a group structure.  -/
Subgroup.toGroup : {G : Type u_3} → [inst : Group G] → (H : Subgroup G) → Group ↥H
-- Mathlib.SetTheory.Ordinal.Notation
/-- Addition of ordinal notations  -/
NONote.instAdd : Add NONote
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.gc_map_comap : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (f : L →ₐ[K] L'),
  GaloisConnection (IntermediateField.map f) (IntermediateField.comap f)
-- Lean.Expr
/-- Counts the number `n` of arguments for an expression `f a₁ .. aₙ`.  -/
Lean.Expr.getAppNumArgs : Lean.Expr → ℕ
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.intPow_negOfNat_bit1 : ∀ {a b c b' c' : ℕ}, a.pow b' = c' → 2 * b' + 1 = b → c' * (c' * a) = c → (Int.negOfNat a).pow b = Int.negOfNat c
-- Lean.Compiler.LCNF.Types
/-- Return `true` if `type` is a LCNF type former type or it is an "any" type.
This function is similar to `isTypeFormerType`, but more liberal.
For example, `isTypeFormerType` returns false for `◾` and `Nat → ◾`, but
this function returns true.
 -/
Lean.Compiler.LCNF.maybeTypeFormerType : Lean.Expr → Bool
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.finsuppSum : ∀ {ι : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Mul M] [inst_2 : Zero β]
  (c : RingCon M) (h h' : ι → β → M) {f g : ι →₀ β},
  (∀ (i : ι), c (h i 0) 0) →
    (∀ (i : ι), c (h' i 0) 0) → (∀ (i : ι), c (h i (f i)) (h' i (g i))) → c (f.sum h) (g.sum h')
-- Init.Data.List.Basic
/-- `l₁ ⊆ l₂` means that every element of `l₁` is also an element of `l₂`, ignoring multiplicity.
 -/
List.Subset : {α : Type u} → List α → List α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- `f` coequalizes the two maps  -/
CategoryTheory.RegularEpi.w_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.RegularEpi f)
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.left (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp self.right (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.pow_eq_top_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MonoidWithZero α] [inst_2 : NoZeroDivisors α] [inst_3 : Nontrivial α]
  {x : WithTop α} {n : ℕ}, x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0
-- Mathlib.Data.Set.Card
Set.ncard_sdiff_add_ncard : ∀ {α : Type u_1} (s t : Set α),
  autoParam s.Finite Set.ncard_sdiff_add_ncard._auto_1 →
    autoParam t.Finite Set.ncard_sdiff_add_ncard._auto_3 → (s \ t).ncard + t.ncard = (s ∪ t).ncard
-- Mathlib.Topology.Constructions.SumProd
/-- Given a neighborhood `s` of `(x, x)`, then `(x, x)` has a square open neighborhood
that is a subset of `s`.  -/
exists_nhds_square : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (X × X)} {x : X},
  s ∈ nhds (x, x) → ∃ U, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s
-- Lean.Meta.AppBuilder
/-- `mkProjection s fieldName` returns an expression for accessing field `fieldName` of the structure `s`.
Remark: `fieldName` may be a subfield of `s`.
 -/
Lean.Meta.mkProjection : Lean.Expr → Lean.Name → Lean.MetaM Lean.Expr
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.natCast_add_of_omega0_le : ∀ {o : Ordinal.{u_4}}, Ordinal.omega0 ≤ o → ∀ (n : ℕ), ↑n + o = o
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The functoriality of `E` with respect to morphisms
in `ComposableArrows ι 3`.  -/
CategoryTheory.Abelian.SpectralObject.map : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    {i' j' k' l' : ι} →
                      (f₁' : i' ⟶ j') →
                        (f₂' : j' ⟶ k') →
                          (f₃' : k' ⟶ l') →
                            (CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶
                                CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃') →
                              (n₀ n₁ n₂ : ℤ) →
                                (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.map._auto_1) →
                                  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.map._auto_3) →
                                    X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.E f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.comp_mapId : ∀ {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.LaxFunctor B C) (G : CategoryTheory.LaxFunctor C D)
  (a : B), (F.comp G).mapId a = CategoryTheory.CategoryStruct.comp (G.mapId (F.obj a)) (G.map₂ (F.mapId a))
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.zoom.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode.Path α → Sort u_2) (path : RBTree.RBNode.Path α)
  (h_1 : (path : RBTree.RBNode.Path α) → motive RBTree.RBNode.nil path)
  (h_2 :
    (n : RBTree.RBNode α) →
      (c : RBTree.RBColor) →
        (a : RBTree.RBNode α) →
          (y : α) →
            (b : RBTree.RBNode α) →
              n = RBTree.RBNode.node c a y b →
                (path : RBTree.RBNode.Path α) → motive (RBTree.RBNode.node c a y b) path),
  (match RBTree.RBNode.nil, path with
    | RBTree.RBNode.nil, path => h_1 path
    | n@h:(RBTree.RBNode.node c a y b), path => h_2 n c a y b h path) =
    h_1 path
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A set `B` is a `G`-block iff the sets of the form `g • B` are pairwise equal or disjoint.  -/
MulAction.IsBlock : (G : Type u_1) → {X : Type u_2} → [SMul G X] → Set X → Prop
-- Mathlib.RingTheory.Localization.Ideal
/-- If `R` is a ring, then prime ideals in the localization at `M`
correspond to prime ideals in the original ring `R` that are disjoint from `M`.
This lemma gives the particular case for an ideal and its map,
see `le_rel_iso_of_prime` for the more general relation isomorphism, and the reverse implication  -/
IsLocalization.isPrime_of_isPrime_disjoint : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (I : Ideal R),
  I.IsPrime → Disjoint ↑M ↑I → (Ideal.map (algebraMap R S) I).IsPrime
-- Lean.Parser.Do
Lean.Parser.Term.letIdDeclNoBinders.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.UInt.BasicAux
UInt64.instOfNat : {n : ℕ} → OfNat UInt64 n
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instTop.eq_1 : ∀ {α : Type u} [inst : AddGroup α],
  AddGroupTopology.instTop = { top := { toTopologicalSpace := ⊤, toIsTopologicalAddGroup := ⋯ } }
-- Lean.Meta.SizeOf
/-- Prove SizeOf spec lemma of the form `sizeOf <ctor-application> = 1 + sizeOf <field_1> + ... + sizeOf <field_n>  -/
Lean.Meta.SizeOfSpecNested.main : Lean.Expr → Lean.Expr → Lean.Meta.SizeOfSpecNested.M Lean.Expr
-- Mathlib.Order.SupClosed
supClosed_singleton : ∀ {α : Type u_3} [inst : SemilatticeSup α] {a : α}, SupClosed {a}
-- Mathlib.Algebra.Ring.Pi
/-- A family of ring homomorphisms `f a : γ →+* β a` defines a ring homomorphism
`RingHom.pi f : γ →+* Π a, β a` given by `RingHom.pi f x b = f b x`.  -/
RingHom.pi : {I : Type u} →
  {f : I → Type u_1} →
    {γ : Type u_2} →
      [inst : (i : I) → NonAssocSemiring (f i)] →
        [inst_1 : NonAssocSemiring γ] → ((i : I) → γ →+* f i) → γ →+* (i : I) → f i
-- Mathlib.Topology.Category.LightProfinite.Basic
lightDiagramToProfinite_obj : ∀ (S : LightDiagram), lightDiagramToProfinite.obj S = S.toProfinite
-- Init.Data.Nat.Bitwise.Lemmas
Nat.zero_xor : ∀ (x : ℕ), 0 ^^^ x = x
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix₂_eq_apply_of_acc : ∀ {α : Sort u_2} {β : α → Sort u_3} {C₂ : (a : α) → β a → Sort u_1} [inst : ∀ (a : α) (b : β a), Nonempty (C₂ a b)]
  {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
  {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b} {a : α} {b : β a},
  Acc R ⟨a, b⟩ →
    WellFounded.partialExtrinsicFix₂ R F a b = F a b fun a' b' x => WellFounded.partialExtrinsicFix₂ R F a' b'
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- An abbreviation of the map which divides an integer vector by an integer.  -/
EisensteinSeries.divIntMap : ℤ → {m : ℕ} → (Fin m → ℤ) → Fin m → ℤ
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sub_sInter_subset : ∀ {α : Type u_2} [inst : Sub α] (s : Set α) (T : Set (Set α)), s - ⋂₀ T ⊆ ⋂ t ∈ T, s - t
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_comp : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {X Y Z : TopModuleCat R} (f : X ⟶ Y) (g : Y ⟶ Z),
  TopModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = TopModuleCat.Hom.hom g ∘SL TopModuleCat.Hom.hom f
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.truth_comp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C} {Z : C}
  (h : 𝒞₂.Ω ⟶ Z),
  CategoryTheory.CategoryStruct.comp 𝒞₁.truth (CategoryTheory.CategoryStruct.comp (𝒞₁.hom 𝒞₂) h) =
    CategoryTheory.CategoryStruct.comp (𝒞₂.χ₀ 𝒞₁.Ω₀) (CategoryTheory.CategoryStruct.comp 𝒞₂.truth h)
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
IsScalarTower.subalgebra : ∀ (R : Type u) (S : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] (S₀ : Subalgebra R S), IsScalarTower (↥S₀) S A
-- Init.System.ST
ST.Ref.h : ∀ {σ α : Type} (self : ST.Ref σ α), Nonempty α
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.mem_inf : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U V : OpenSubgroup G} {x : G},
  x ∈ U ⊓ V ↔ x ∈ U ∧ x ∈ V
-- Mathlib.Algebra.Group.Action.Defs
vadd_vadd_vadd_comm : ∀ {α : Type u_5} {β : Type u_6} {γ : Type u_7} {δ : Type u_8} [inst : VAdd α β] [inst_1 : VAdd α γ] [inst_2 : VAdd β δ]
  [inst_3 : VAdd α δ] [inst_4 : VAdd γ δ] [VAddAssocClass α β δ] [VAddAssocClass α γ δ] [VAddCommClass β γ δ] (a : α)
  (b : β) (c : γ) (d : δ), (a +ᵥ b) +ᵥ c +ᵥ d = (a +ᵥ c) +ᵥ b +ᵥ d
-- Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
CategoryTheory.instPreservesMonomorphismsFunctorObjWhiskeringRight : ∀ {K : Type u} [inst : CategoryTheory.Category.{v, u} K] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {D : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasPullbacks C]
  (F : CategoryTheory.Functor C D) [F.PreservesMonomorphisms],
  ((CategoryTheory.Functor.whiskeringRight K C D).obj F).PreservesMonomorphisms
-- Mathlib.Data.Sum.Order
Sum.Lex.inl_le_inl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : α}, toLex (Sum.inl a) ≤ toLex (Sum.inl b) ↔ a ≤ b
-- Mathlib.RingTheory.Coalgebra.Basic
DFinsupp.counit_single : ∀ (R : Type u) (ι : Type v) (A : ι → Type w) [inst : DecidableEq ι] [inst_1 : CommSemiring R]
  [inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : (i : ι) → Module R (A i)]
  [inst_4 : (i : ι) → CoalgebraStruct R (A i)] (i : ι) (a : A i),
  (CoalgebraStruct.counit fun₀ | i => a) = CoalgebraStruct.counit a
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.subsingleton : ∀ {α : Type u} [inst : TopologicalSpace α] [PreconnectedSpace α], Subsingleton (ConnectedComponents α)
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.intCast_def : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : AddCommGroupWithOne A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoidWithOne B] [inst_4 : Module R B] (z : ℤ), ↑z = ↑z ⊗ₜ[R] 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The forgetful functor from lax braided functors to lax monoidal functors.  -/
CategoryTheory.LaxBraidedFunctor.forget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                CategoryTheory.Functor (CategoryTheory.LaxBraidedFunctor C D) (CategoryTheory.LaxMonoidalFunctor C D)
-- Init.Data.Ord.Basic
Ordering.lt_beq_eq : (Ordering.lt == Ordering.eq) = false
-- Mathlib.Data.Nat.ChineseRemainder
Quotient.recOn.congr_simp : ∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (q : Quotient s) (f f_1 : (a : α) → motive ⟦a⟧)
  (e_f : f = f_1) (h : ∀ (a b : α) (p : a ≈ b), ⋯ ▸ f a = f b), Quotient.recOn q f h = Quotient.recOn q f_1 ⋯
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertMany_list_eq_empty_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)}, m.insertMany l = ∅ ↔ m = ∅ ∧ l = []
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.digitChar.eq_1 : ∀ (n : ℕ),
  n.digitChar =
    if n = 0 then '0'
    else
      if n = 1 then '1'
      else
        if n = 2 then '2'
        else
          if n = 3 then '3'
          else
            if n = 4 then '4'
            else
              if n = 5 then '5'
              else
                if n = 6 then '6'
                else
                  if n = 7 then '7'
                  else
                    if n = 8 then '8'
                    else
                      if n = 9 then '9'
                      else
                        if n = 10 then 'a'
                        else
                          if n = 11 then 'b'
                          else
                            if n = 12 then 'c'
                            else if n = 13 then 'd' else if n = 14 then 'e' else if n = 15 then 'f' else '*'
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ordHom.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] (z z_1 : ↥X) (e_z : z = z_1) (hz : Order.coheight z = 1),
  AlgebraicGeometry.Scheme.ordHom z hz = AlgebraicGeometry.Scheme.ordHom z_1 ⋯
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.rankTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.HeapNode α → ℕ → Sort u_2) (r : ℕ)
  (h_1 : (r : ℕ) → motive Batteries.BinomialHeap.Imp.HeapNode.nil r)
  (h_2 :
    (a : α) →
      (child s : Batteries.BinomialHeap.Imp.HeapNode α) →
        (r : ℕ) → motive (Batteries.BinomialHeap.Imp.HeapNode.node a child s) r),
  (match Batteries.BinomialHeap.Imp.HeapNode.nil, r with
    | Batteries.BinomialHeap.Imp.HeapNode.nil, r => h_1 r
    | Batteries.BinomialHeap.Imp.HeapNode.node a child s, r => h_2 a child s r) =
    h_1 r
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.refl : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] (d : PseudoMetric X R) (x : X),
  d x x = 0
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.equivProd_apply : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (x : N ⋊[φ] G),
  SemidirectProduct.equivProd x = (x.left, x.right)
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- If the `ChartedSpace` structure on a manifold `M` is given by an open embedding `e : M → H`,
then the inverse of `e` is `C^n`.  -/
contMDiffOn_isOpenEmbedding_symm : ∀ {𝕜 : 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] {e : M → H} (h : Topology.IsOpenEmbedding e) {n : WithTop ℕ∞} [inst_5 : Nonempty M],
  ContMDiffOn I I n (↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph e h).symm) (Set.range e)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.ι_fromFreeYonedaCoproduct_assoc : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (m : M.Elements) {Z : PresheafOfModules R} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (M.ιFreeYonedaCoproduct m)
      (CategoryTheory.CategoryStruct.comp M.fromFreeYonedaCoproduct h) =
    CategoryTheory.CategoryStruct.comp m.fromFreeYoneda h
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_inv : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α],
  (CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).counitIso.inv = CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Binary entropy has derivative `log (1 - p) - log p`.
It's not differentiable at `0` or `1` but the junk values of `deriv` and `log` coincide there.  -/
Real.deriv_binEntropy : ∀ (p : ℝ), deriv Real.binEntropy p = Real.log (1 - p) - Real.log p
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul' : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  UniformContinuousConstSMul R (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- A commutative group object is a commutative monoid object.  -/
CategoryTheory.CommGrp.toCommMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommGrp C → CategoryTheory.CommMon C
-- Mathlib.RingTheory.Ideal.IsAugmentation
Ideal.IsAugmentation.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A] (I : Ideal A),
  Ideal.IsAugmentation R I = IsCompl 1 (Submodule.restrictScalars R I)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `g` and `h` commute, then `g` moves `h • x` iff `g` moves `x`.
This is equivalent to say that the set `(fixedBy α g)ᶜ` is fixed by `h`.
 -/
MulAction.movedBy_mem_fixedBy_of_commute : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g h : G},
  Commute g h → (MulAction.fixedBy α g)ᶜ ∈ MulAction.fixedBy (Set α) h
-- Mathlib.Order.Filter.Defs
/-- `f.IsBoundedUnder (≺) u`: the image of the filter `f` under `u` is eventually bounded w.r.t.
the relation `≺`, i.e. eventually, it is bounded by some uniform bound.  -/
Filter.IsBoundedUnder : {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → Filter β → (β → α) → Prop
-- Init.Data.String.Slice
/-- Finds the position of the first match of the pattern `pat` in a slice, starting
from the end of the slice and traversing towards the start. If there is no match `none` is
returned.

This function is generic over all currently supported patterns except
`String`/`String.Slice`.

Examples:

* `("coffee tea water".toSlice.revFind? Char.isWhitespace).map (·.get!) == some ' '`

* `"tea".toSlice.revFind? (fun (c : Char) => c == 'X') == none`
 -/
String.Slice.revFind? : {σ : String.Slice → Type} →
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
    [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
      {ρ : Type} → (s : String.Slice) → (pat : ρ) → [String.Slice.Pattern.ToBackwardSearcher pat σ] → Option s.Pos
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_C_mul_X_pow : ∀ {R : Type u} {a : R} [inst : Semiring R] (n : ℕ), a ≠ 0 → (Polynomial.C a * Polynomial.X ^ n).trailingDegree = ↑n
-- Lean.Meta.Tactic.Grind.Proof
/-- Given `h : a ≍ b`, returns a proof `a = b` if `heq == false`.
Otherwise, it returns `h`.
 -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkEqOfHEqIfNeeded : Lean.Expr → Bool → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.Subgroup.genLTOne.eq_1 : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G] (H : Subgroup G)
  [inst_3 : Nontrivial ↥H] [hH : IsCyclic ↥H], LinearOrderedCommGroup.Subgroup.genLTOne H = ⋯.choose
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeLift_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {t₁ t₂ : CategoryTheory.Limits.Cocone K}
  (f : t₁ ⟶ t₂), (CategoryTheory.WithInitial.coconeLift✝.map f).hom = CategoryTheory.Under.Hom.right f.hom
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_lt_one_add : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℤ_[p]}, ‖z1‖ < 1 → ‖z2‖ < 1 → ‖z1 + z2‖ < 1
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.SynthM : Type → Type
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.trCfg.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {Λ : Type u_2} [inst_1 : Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (q : Λ)
  (T : Turing.Tape Γ),
  Turing.TM0to1.trCfg M { q := q, Tape := T } =
    { l := bif (M q T.head).isSome then some (Turing.TM0to1.Λ'.normal q) else none, var := (), Tape := T }
-- Mathlib.RingTheory.Ideal.Defs
Ideal.IsTwoSided.mul_mem_of_left : ∀ {α : Type u} {inst : Semiring α} {I : Ideal α} [self : I.IsTwoSided] {a : α} (b : α), a ∈ I → a * b ∈ I
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the reverse direction of `Order.pred_lt_iff_not_isMin`. -/
Order.pred_lt_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, ¬IsMin a → Order.pred a < a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedLitValue.default : Lean.Compiler.LCNF.LitValue
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_sub : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Ring R] (v : AbsoluteValue R S)
  (x y : R), WithAbs.toAbs v (x - y) = WithAbs.toAbs v x - WithAbs.toAbs v y