mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.coeff_frobenius_charP : ∀ (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x : WittVector p R) (n : ℕ),
  (WittVector.frobenius x).coeff n = x.coeff n ^ p
-- Mathlib.Analysis.Calculus.ContDiff.Defs
Filter.EventuallyEq.congr_contDiffWithinAt_of_insert : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  f₁ =ᶠ[nhdsWithin x (insert x s)] f → (ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x)
-- Mathlib.CategoryTheory.PathCategory.Basic
_private.Mathlib.CategoryTheory.PathCategory.Basic.0.CategoryTheory.composePath.match_1.eq_1 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} (motive : (x : C) → Quiver.Path X x → Sort u_3)
  (h_1 : Unit → motive X Quiver.Path.nil) (h_2 : (x b : C) → (p : Quiver.Path X b) → (e : b ⟶ x) → motive x (p.cons e)),
  (match X, Quiver.Path.nil with
    | .(X), Quiver.Path.nil => h_1 ()
    | x, p.cons e => h_2 x b p e) =
    h_1 ()
-- Mathlib.Data.Holor
Holor.CPRankMax1.cons : ∀ {α : Type} [inst : Mul α] {d : ℕ} {ds : List ℕ} (x : Holor α [d]) (y : Holor α ds),
  y.CPRankMax1 → (x.mul y).CPRankMax1
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsAddIndecomposable.mem_or_neg_mem_closure_baseOf : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : AddCommGroup G] [inst_1 : LinearOrder S] [Finite ι]
  [inst_3 : InvolutiveNeg ι] [inst_4 : AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G) (f : G →+ S) (i : ι),
  f (v i) ≠ 0 →
    v (-i) = -v i →
      v i ∈ AddSubmonoid.closure (v '' IsAddIndecomposable.baseOf v f) ∨
        -v i ∈ AddSubmonoid.closure (v '' IsAddIndecomposable.baseOf v f)
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
CategoryTheory.Functor.congr_isDenseAt : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G), F.isDenseAt = G.isDenseAt
-- Mathlib.Data.TypeVec
TypeVec.nilFun_comp : ∀ {α₀ : TypeVec.{u_1} 0} (f₀ : α₀.Arrow Fin2.elim0), TypeVec.comp TypeVec.nilFun f₀ = f₀
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_coe_toAddMonoidHom : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M),
  AddSubmonoid.map (↑f) S = AddSubmonoid.map f S
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.HasLeftCalculusOfFractions] ⦃X Y : C⦄ (φ : W.RightFraction X Y),
  ∃ ψ, CategoryTheory.CategoryStruct.comp φ.f ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Metric.ediam_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (s : Set α), Metric.ediam (closure s) = Metric.ediam s
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinAlgEquiv'_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  Matrix.toLinAlgEquiv'.symm = LinearMap.toMatrixAlgEquiv'
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm : ∀ {R : Type u} [inst : CommRing R] (s : TopologicalSpace.Clopens (PrimeSpectrum R)),
  PrimeSpectrum.basicOpen ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s) = s.toOpens
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mk : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            {f g : C ⟶ D} →
              (hom : (i j : ι) → C.X i ⟶ D.X j) →
                autoParam (∀ (i j : ι), ¬c.Rel j i → hom i j = 0) Homotopy.zero._autoParam →
                  autoParam (∀ (i : ι), f.f i = (dNext i) hom + (prevD i) hom + g.f i) Homotopy.comm._autoParam →
                    Homotopy f g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S}
  (self : h.LiftStruct g₁ g₂ b) {Z : C} (h_1 : X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp h.p₂ h_1) =
    CategoryTheory.CategoryStruct.comp g₂ h_1
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.natDegree_integralNormalization : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.integralNormalization.natDegree = p.natDegree
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- The left part of an adjoint quadruple `L ⊣ F ⊣ G ⊣ R`.  -/
CategoryTheory.Adjunction.Quadruple.leftTriple : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {F : CategoryTheory.Functor D C} →
            {G : CategoryTheory.Functor C D} →
              {R : CategoryTheory.Functor D C} →
                CategoryTheory.Adjunction.Quadruple L F G R → CategoryTheory.Adjunction.Triple L F G
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Get the largest element in the tree that is `< x`.

```
findLt 2 {1, 2, 4} = some 1
findLt 3 {1, 2, 4} = some 2
findLt 0 {1, 2, 4} = none
```  -/
Ordnode.findLt : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Option α
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.apply_inr : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} {l : Combinatorics.Subspace η α ι} {x : η → α} {i : ι} {e : η},
  l.idxFun i = Sum.inr e → ↑l x i = x e
-- Mathlib.Order.MinMax
min_max_distrib_right : ∀ {α : Type u} [inst : LinearOrder α] (a b c : α), min (max a b) c = max (min a c) (min b c)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
/-- The (exact) short complex `H^n₀(g) ⟶ H^n₁(f) ⟶ H^n₁(fg)` of a
spectral object, when `f ≫ g = fg` and `n₀ + 1 = n₁`.  -/
CategoryTheory.Abelian.SpectralObject.sc₁ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) →
                    CategoryTheory.CategoryStruct.comp f g = fg →
                      (n₀ n₁ : ℤ) →
                        autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₁._auto_1 →
                          CategoryTheory.ShortComplex C
-- Mathlib.Data.Vector.Defs
List.Vector.toList_getElem : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n) (i : ℕ) {hi : i < v.toList.length}, v.toList[i] = v[i]
-- Init.Data.Repr
/-- Returns a single digit representation of `n`, which is assumed to be in a base less than or equal to
`16`. Returns `'*'` if `n > 15`.

Examples:
 * `Nat.digitChar 5 = '5'`
 * `Nat.digitChar 12 = 'c'`
 * `Nat.digitChar 15 = 'f'`
 * `Nat.digitChar 16 = '*'`
 * `Nat.digitChar 85 = '*'`
 -/
Nat.digitChar : ℕ → Char
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_injective : ∀ {n : ℕ}, Function.Injective SimplexCategory.δ
-- Lean.Parser.Types
Lean.Parser.ParserCacheKey.pos : Lean.Parser.ParserCacheKey → String.Pos.Raw
-- Mathlib.Order.BoundedOrder.Lattice
min_eq_bot : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderBot α] {a b : α}, min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Composition of a conjugate square with a square between left adjoints.  -/
CategoryTheory.Bicategory.leftAdjointConjugateSquare.vcomp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      {g : a ⟶ c} →
        {h : b ⟶ d} →
          {l₁ l₂ : a ⟶ b} →
            {l₃ : c ⟶ d} →
              (l₂ ⟶ l₁) →
                (CategoryTheory.CategoryStruct.comp g l₃ ⟶ CategoryTheory.CategoryStruct.comp l₂ h) →
                  (CategoryTheory.CategoryStruct.comp g l₃ ⟶ CategoryTheory.CategoryStruct.comp l₁ h)
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.norm_toL1 : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β) (hf : MeasureTheory.Integrable f μ),
  ‖MeasureTheory.Integrable.toL1 f hf‖ = (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.descentData_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (D : F.DescentData' sq sq₃) (x : C) (x_1 : x ⟶ S) (x_2 x_3 : ι) (x_4 : x ⟶ X x_2) (x_5 : x ⟶ X x_3)
  (x_6 : CategoryTheory.CategoryStruct.comp x_4 (f x_2) = x_1)
  (x_7 : CategoryTheory.CategoryStruct.comp x_5 (f x_3) = x_1),
  D.descentData.hom x_1 x_4 x_5 x_6 x_7 =
    CategoryTheory.Pseudofunctor.DescentData'.pullHom' D.hom (CategoryTheory.CategoryStruct.comp x_4 (f x_2)) x_4 x_5 ⋯
      ⋯
-- Mathlib.Data.Ordering.Lemmas
cmpUsing_eq_lt : ∀ {α : Type u} {lt : α → α → Prop} [inst : DecidableRel lt] (a b : α), (cmpUsing lt a b = Ordering.lt) = lt a b
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.coe_coe : ∀ {R : Type u_1} [inst : AddGroupWithOne R] {f : ArithmeticFunction ℕ}, ↑↑f = ↑f
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.zsmul : {α : Type u} → [inst : Lean.Grind.Semiring α] → ℤ → Lean.Grind.Ring.OfSemiring.Q α → Lean.Grind.Ring.OfSemiring.Q α
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
/-- Assuming `G` is strongly regular, `2*(k + 1) - m` in `G` is the number of vertices that are
adjacent to either `v` or `w` when `¬G.Adj v w`. So it's the cardinality of
`G.neighborSet v ∪ G.neighborSet w`.  -/
SimpleGraph.IsSRGWith.card_neighborFinset_union_of_not_adj : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V] {v w : V},
  G.IsSRGWith n k ℓ μ → v ≠ w → ¬G.Adj v w → (G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - μ
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_intCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIcoMod hp (a - ↑m * p) b = toIcoMod hp a b - ↑m * p
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- The `nnnorm` of a function is controlled by the supremum of the pointwise `nnnorm`s.  -/
BoundedContinuousFunction.nnnorm_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β) (C : NNReal), ‖f‖₊ ≤ C ↔ ∀ (x : α), ‖f x‖₊ ≤ C
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.uniqueMDiffOn_preimage : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  n ≠ 0 → ∀ {s : Set N}, UniqueMDiff[⇑h ⁻¹' s] ↔ UniqueMDiff[s]
-- Mathlib.RingTheory.MatrixAlgebra
/-- `Matrix.kronecker` as a linear equivalence, when the two arguments are tensored.  -/
kroneckerLinearEquiv : (l : Type u_1) →
  (m : Type u_2) →
    (n : Type u_3) →
      (p : Type u_4) →
        (R : Type u_5) →
          [inst : CommSemiring R] →
            [Fintype l] →
              [Fintype m] →
                [Fintype n] →
                  [Fintype p] →
                    [DecidableEq l] →
                      [DecidableEq m] →
                        [DecidableEq n] →
                          [DecidableEq p] → TensorProduct R (Matrix l m R) (Matrix n p R) ≃ₗ[R] Matrix (l × n) (m × p) R
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
/-- Let `F` be a locally directed diagram of open immersions, i.e., a diagram of schemes
for which whenever `xᵢ ∈ Fᵢ` and `xⱼ ∈ Fⱼ` map to the same `xₖ ∈ Fₖ`, there exists
some `xₗ ∈ Fₗ` that maps to `xᵢ` and `xⱼ` (e.g, the diagram indexing a coproduct).
Then the colimit inclusions are a Zariski covering.  -/
AlgebraicGeometry.ofArrows_ι_mem_zariskiTopology_of_isColimit : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, u_1} J]
  (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Sieve.ofArrows F.obj c.ι.app ∈ AlgebraicGeometry.Scheme.zariskiTopology c.pt
-- Mathlib.RingTheory.SimpleModule.Basic
LinearMap.surjective_of_ne_zero : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSimpleModule R N] {f : M →ₗ[R] N}, f ≠ 0 → Function.Surjective ⇑f
-- Init.Data.String.Pattern.Basic
/-- Checks whether the slice starts with the pattern. If it does, the slice is returned with the
  prefix removed; otherwise the result is `none`.
   -/
String.Slice.Pattern.ForwardPattern.skipPrefix? : {ρ : Type} → (pat : ρ) → [self : String.Slice.Pattern.ForwardPattern pat] → (s : String.Slice) → Option s.Pos
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).minKey ⋯ = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.neg_of_mem_negA_plusPart : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} (A : Set (NumberField.mixedEmbedding.mixedSpace K))
  {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ ⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A →
    ∀ {w : { w // w.IsReal }}, w ∈ s → x.1 w < 0
-- Mathlib.Logic.Equiv.Fin.Rotate
coe_finRotate : ∀ {n : ℕ} (i : Fin n.succ), ↑((finRotate n.succ) i) = if i = Fin.last n then 0 else ↑i + 1
-- Mathlib.Logic.Relation
Relation.EqvGen.eqvGen_reflTransGen : ∀ {α : Type u_1} (r : α → α → Prop), Relation.EqvGen (Relation.ReflTransGen r) = Relation.EqvGen r
-- Init.Data.Char.Ordinal
Char.ofOrdinal_inj : ∀ {f g : Fin Char.numCodePoints}, Char.ofOrdinal f = Char.ofOrdinal g ↔ f = g
-- Mathlib.Algebra.Order.Sub.Defs
lt_tsub_comm : ∀ {α : Type u_1} {a b c : α} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α],
  a < b - c ↔ c < b - a
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientSubgroupOfMapOfLE.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (H : Subgroup α) (h : s ≤ t),
  Subgroup.quotientSubgroupOfMapOfLE H h = Quotient.map' id ⋯
-- Lean.Meta.LitValues
/-- Check if an expression is a list literal (i.e. a nested chain of `List.cons`, ending at a `List.nil`),
returning the array of `Expr` values.
 -/
Lean.Meta.getListLit? : Lean.Expr → Lean.MetaM (Option (Array Lean.Expr))
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (Y : C) {n₀ : ℕ}
  (x₁ : CategoryTheory.Abelian.Ext S.X₁ Y n₀) {n₁ : ℕ} (hn₁ : 1 + n₀ = n₁),
  hS.extClass.comp x₁ hn₁ = 0 → ∃ x₂, (CategoryTheory.Abelian.Ext.mk₀ S.f).comp x₂ ⋯ = x₁
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_const_pure : ∀ {α : Type u_1} {β : Type u_2} {a : Filter α} {b : β}, Filter.Tendsto (fun x => b) a (pure b)
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- Inversion is smooth in a Lie group.  -/
LieGroup.contMDiff_inv : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} {inst_4 : Group G} {inst_5 : TopologicalSpace G} {inst_6 : ChartedSpace H G} [self : LieGroup I n G],
  ContMDiff I I n fun a => a⁻¹
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
pentagonal_strictAntiOn : StrictAntiOn pentagonal (Set.Iic 0)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.equiv_iff_toList_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.symm_mem_transvections_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {e : V ≃ₗ[R] V},
  e.symm ∈ LinearEquiv.transvections R V ↔ e ∈ LinearEquiv.transvections R V
-- Mathlib.Logic.Equiv.Prod
Equiv.uniqueSigma_symm_apply : ∀ {α : Type u_10} {β : α → Type u_9} [inst : Unique α] (y : β default), (Equiv.uniqueSigma β).symm y = ⟨default, y⟩
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- The `V`-enriched hom from `F₁` to `F₂` when `F₁` and `F₂` are functors `J ⥤ C`
and `C` is a `V`-enriched category.  -/
CategoryTheory.Enriched.FunctorCategory.enrichedHom : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                (F₁ F₂ : CategoryTheory.Functor J C) →
                  [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] → V
-- Mathlib.CategoryTheory.Presentable.Dense
CategoryTheory.isCardinalFilteredGenerator_isCardinalPresentable : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalAccessibleCategory C κ],
  (CategoryTheory.isCardinalPresentable C κ).IsCardinalFilteredGenerator κ
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.supportDim R M = Order.krullDim ↑(Module.support R M)
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instDistribSMulAEEqFun : {M : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : SMul M α] →
              [MeasurableConstSMul M α] →
                [MeasureTheory.SMulInvariantMeasure M α μ] →
                  [inst_5 : AddMonoid β] → [inst_6 : ContinuousAdd β] → DistribSMul Mᵈᵐᵃ (α →ₘ[μ] β)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- On a set with unique differentiability, an analytic function is automatically `C^ω`, as its
successive derivatives are also analytic. This does not require completeness of the space. See
also `AnalyticOn.contDiffOn_of_completeSpace`.  -/
AnalyticOn.contDiffOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, AnalyticOn 𝕜 f s → UniqueDiffOn 𝕜 s → ContDiffOn 𝕜 n f s
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_iff_ne_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α} [inst_2 : OrderTop α], a < Order.succ a ↔ a ≠ ⊤
-- Mathlib.Data.Finset.NAry
Finset.image₂_swap : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β),
  Finset.image₂ f s t = Finset.image₂ (fun a b => f b a) t s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.whiskerLeft_η_commutator_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.GrpObj G] {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G CategoryTheory.MonObj.one)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrpObj.commutator G) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.toUnit
        (CategoryTheory.MonoidalCategoryStruct.tensorObj G (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
-- Mathlib.Algebra.Polynomial.Laurent
/-- To prove something about Laurent polynomials, it suffices to show that
* the condition is closed under taking sums, and
* it holds for monomials.
 -/
LaurentPolynomial.induction_on' : ∀ {R : Type u_1} [inst : Semiring R] {motive : LaurentPolynomial R → Prop} (p : LaurentPolynomial R),
  (∀ (p q : LaurentPolynomial R), motive p → motive q → motive (p + q)) →
    (∀ (n : ℤ) (a : R), motive (LaurentPolynomial.C a * LaurentPolynomial.T n)) → motive p
-- Init.Data.UInt.Bitwise
Bool.toUInt64.eq_1 : ∀ (b : Bool), b.toUInt64 = if b = true then 1 else 0
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.min_le_min_add : ∀ {R : Type u_3} [inst : AddMonoid R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R} (hx : x ≠ 0)
  (hy : y ≠ 0) (hxy : x + y ≠ 0), min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- The coercion `(B · ·) : E → (F → 𝕜)` is an embedding.  -/
LinearMap.IsWeak.isEmbedding : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} [hB : B.IsWeak],
  Function.Injective ⇑B → Topology.IsEmbedding fun x1 x2 => (B x1) x2
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Given `x : R` and a localization map `F : R →+* S` away from `x`, `invSelf` is `(F x)⁻¹`.  -/
IsLocalization.Away.invSelf : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → (x : R) → [IsLocalization.Away x S] → S
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instMonadReaderOfSubExprAnalyzeM : MonadReaderOf Lean.SubExpr Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- The product of two normed spaces is a normed space, with the `L^p` norm.  -/
WithLp.instProdNormedSpace : (p : ENNReal) →
  (𝕜 : Type u_1) →
    (α : Type u_2) →
      (β : Type u_3) →
        [hp : Fact (1 ≤ p)] →
          [inst : SeminormedAddCommGroup α] →
            [inst_1 : SeminormedAddCommGroup β] →
              [inst_2 : NormedField 𝕜] → [NormedSpace 𝕜 α] → [NormedSpace 𝕜 β] → NormedSpace 𝕜 (WithLp p (α × β))
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.natDegree_intCast_le : ∀ {R : Type u_1} [inst : Ring R] (n : ℤ), (↑n).natDegree ≤ 0
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.below : {motive : (m : ℕ) → (L : List ℕ) → SimplexCategoryGenRel.IsAdmissible m L → Prop} →
  {m : ℕ} → {L : List ℕ} → SimplexCategoryGenRel.IsAdmissible m L → Prop