mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fintype.Card
/-- A `Fintype` with cardinality zero is equivalent to `Empty`.  -/
Fintype.cardEqZeroEquivEquivEmpty : {α : Type u_1} → [inst : Fintype α] → Fintype.card α = 0 ≃ (α ≃ Empty)
-- Init.Data.String.Lemmas.Order
String.Pos.get_slice : ∀ {s : String} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁} {h : p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).endPos},
  (p.slice p₀ p₁ h₁ h₂).get h = p.get ⋯
-- Mathlib.Data.Matrix.Basic
/-- A version of `Set.matrix` for `Submodule`s.
Given a `Submodule` `S`, `S.matrix` is the `Submodule` of matrices `m`
all of whose entries `m i j` belong to `S`.  -/
Submodule.matrix : {m : Type u_2} →
  {n : Type u_3} →
    {R : Type u_14} →
      {M : Type u_15} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Submodule R (Matrix m n M)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instSupSet : {R : Type u} → {M : Type v} → [inst : VAdd R M] → SupSet (SubAddAction R M)
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConsts.mk.inj : ∀ {size : ℕ} {revList : List Lean.AsyncConst✝} {map : Lean.NameMap Lean.AsyncConst✝}
  {normalizedTrie : Lean.NameTrie Lean.AsyncConst✝} {size_1 : ℕ} {revList_1 : List Lean.AsyncConst✝}
  {map_1 : Lean.NameMap Lean.AsyncConst✝} {normalizedTrie_1 : Lean.NameTrie Lean.AsyncConst✝},
  { size := size, revList := revList, map := map, normalizedTrie := normalizedTrie } =
      { size := size_1, revList := revList_1, map := map_1, normalizedTrie := normalizedTrie_1 } →
    size = size_1 ∧ revList = revList_1 ∧ map = map_1 ∧ normalizedTrie = normalizedTrie_1
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_comp_rev : ∀ {α : Sort u_1} {m n : ℕ} (xs : Fin m → α) (ys : Fin n → α),
  Fin.append xs ys ∘ Fin.rev = Fin.append (ys ∘ Fin.rev) (xs ∘ Fin.rev) ∘ Fin.cast ⋯
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The product of a family of partial equivalences, as a partial equivalence on the pi type.  -/
PartialEquiv.pi : {ι : Type u_5} →
  {αi : ι → Type u_6} →
    {βi : ι → Type u_7} → ((i : ι) → PartialEquiv (αi i) (βi i)) → PartialEquiv ((i : ι) → αi i) ((i : ι) → βi i)
-- Init.Data.List.Count
_private.Init.Data.List.Count.0.List.findIdx.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) → ((n : ℕ) → motive [] n) → ((a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n) → motive x x_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- An equivalence from `WalkingPair` to `Bool`, sometimes useful when reindexing limits.
 -/
CategoryTheory.Limits.WalkingPair.equivBool : CategoryTheory.Limits.WalkingPair ≃ Bool
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.coe_nsmul : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddMonoid (β i)] (b : ℕ) (v : Π₀ (i : ι), β i), ⇑(b • v) = b • ⇑v
-- Mathlib.Topology.Order.LocalExtr
isLocalMinOn_const : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {a : α} {b : β},
  IsLocalMinOn (fun x => b) s a
-- Mathlib.Topology.Instances.ENat
ENat.isEmbedding_natCast : Topology.IsEmbedding Nat.cast
-- Lean.Expr
/-- Return `true` if the given expression is a literal value.  -/
Lean.Expr.isLit : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- The wedge defined by `π` and `hπ` is a limit wedge, i.e `H.obj c` is
an end of `internalHomDiagramFunctor F G|>.obj c`.  -/
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.isLimitWedge : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            [inst_4 : CategoryTheory.MonoidalClosed V] →
              {F G H : CategoryTheory.Functor C V} →
                (self : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) →
                  (c : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Wedge.mk (H.obj c) (self.π c) ⋯)
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.stalkClosedPointTo_comp : ∀ {X Y : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X)
  (g : X ⟶ Y),
  AlgebraicGeometry.Scheme.stalkClosedPointTo (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap g (f (IsLocalRing.closedPoint ↑R)))
      (AlgebraicGeometry.Scheme.stalkClosedPointTo f)
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- **Alias** of `PointedCone.mem_hull_set`.

---

Elements of the cone hull are expressible as conical combination of elements from s.  -/
PointedCone.mem_span_set : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {x : E} {s : Set E},
  x ∈ PointedCone.hull R s ↔ ∃ c, ↑c.support ⊆ s ∧ (∀ (y : E), 0 ≤ c y) ∧ (c.sum fun m r => r • m) = x
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
/-- An `A`-submodule `p ⊆ M` is homogeneous if for every `m ∈ p`, all homogeneous components of `m` are
in `p`.
 -/
Submodule.IsHomogeneous : {ιM : Type u_2} →
  {σM : Type u_4} →
    {A : Type u_5} →
      {M : Type u_6} →
        [inst : Semiring A] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module A M] →
              Submodule A M →
                (ℳ : ιM → σM) →
                  [inst : DecidableEq ιM] →
                    [inst_3 : SetLike σM M] → [inst_4 : AddSubmonoidClass σM M] → [DirectSum.Decomposition ℳ] → Prop
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C}
  {A : C} {toPrepathObject : HomotopicalAlgebra.PrepathObject A}
  {weakEquivalence_ι :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrepathObject.ι)
      HomotopicalAlgebra.PathObject.weakEquivalence_ι._autoParam}
  {toPrepathObject_1 : HomotopicalAlgebra.PrepathObject A}
  {weakEquivalence_ι_1 :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrepathObject_1.ι)
      HomotopicalAlgebra.PathObject.weakEquivalence_ι._autoParam},
  { toPrepathObject := toPrepathObject, weakEquivalence_ι := weakEquivalence_ι } =
      { toPrepathObject := toPrepathObject_1, weakEquivalence_ι := weakEquivalence_ι_1 } →
    toPrepathObject = toPrepathObject_1
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.mkD_of_not_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {g : C(α, β)},
  ¬Continuous f → ContinuousMap.mkD f g = g
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rxc.Iterator.Monadic.step.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → (Unit → motive none) → ((next : α) → motive (some next)) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteEdges_adj : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) (v w : V),
  (G'.deleteEdges s).Adj v w ↔ G'.Adj v w ∧ s(v, w) ∉ s
-- Lean.Parser.Basic
Lean.Parser.sepByNoAntiquot : Lean.Parser.Parser → Lean.Parser.Parser → optParam Bool false → Lean.Parser.Parser
-- Mathlib.RingTheory.AdicCompletion.RingHom
/-- The composition of lift linear map `lift I f hf : R →+* S` with the canonical
projection `S →+* S ⧸ (I ^ n)` is `f n` .
 -/
IsAdicComplete.mk_liftRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  [inst_2 : IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) (n : ℕ) (x : R),
  (Ideal.Quotient.mk (I ^ n)) ((IsAdicComplete.liftRingHom I f ⋯) x) = (f n) x
-- Mathlib.RingTheory.Trace.Basic
/-- `embeddingsMatrixReindex A C b e : Matrix κ κ C` is the matrix whose `(i, j)` coefficient
is `σⱼ (b i)`, where `σⱼ : B →ₐ[A] C` is the embedding corresponding to `j : κ` given by a
bijection `e : κ ≃ (B →ₐ[A] C)`. It is mostly useful for fields and `C` is algebraically closed.
In this case, in presence of `h : Fintype.card κ = finrank A B`, one can take
`e := equivOfCardEq ((AlgHom.card A B C).trans h.symm)`.  -/
Algebra.embeddingsMatrixReindex : {κ : Type w} →
  (A : Type u) →
    {B : Type v} →
      (C : Type z) →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [inst_2 : Algebra A B] →
              [inst_3 : CommRing C] → [inst_4 : Algebra A C] → (κ → B) → κ ≃ (B →ₐ[A] C) → Matrix κ κ C
-- Lean.Meta.Tactic.Assumption
/-- Return a local declaration whose type is definitionally equal to `type`.  -/
Lean.Meta.findLocalDeclWithType? : Lean.Expr → Lean.MetaM (Option Lean.FVarId)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.mem_node : ∀ {α : Type u_1} {y : α} {c : RBTree.RBColor} {a : RBTree.RBNode α} {x : α} {b : RBTree.RBNode α},
  y ∈ RBTree.RBNode.node c a x b ↔ y = x ∨ y ∈ a ∨ y ∈ b
-- Mathlib.CategoryTheory.Presentable.StrongGenerator
CategoryTheory.ObjectProperty.isFiltered_costructuredArrow_colimitsCardinalClosure_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (κ : Cardinal.{w})
  [Fact κ.IsRegular] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] (X : C),
  CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow (P.colimitsCardinalClosure κ).ι X)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- Given a Type `R` with instances for each of the `Ring` operations, make a
`Language.ring.Structure R` instance, along with a proof that the operations given
by the `Language.ring.Structure` are the same as those given by the `Add` or `Mul` etc.
instances.

This definition can be used when applying a theorem about the model theory of rings
to a literal ring `R`, by writing `let _ := compatibleRingOfRing R`. After this, if,
for example, `R` is a field, then Lean will be able to find the instance for
`Theory.field.Model R`, and it will be possible to apply theorems about the model theory
of fields.

This is a `def` and not an `instance`, because the path
`Ring` => `Language.ring.Structure` => `Ring` cannot be made to
commute by definition
 -/
FirstOrder.Ring.compatibleRingOfRing : (R : Type u_2) →
  [inst : Add R] →
    [inst_1 : Mul R] → [inst_2 : Neg R] → [inst_3 : One R] → [inst_4 : Zero R] → FirstOrder.Ring.CompatibleRing R
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_indicator₂ : ∀ (α : Type u_1) (G : Type u_5) [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {β : Type u_6} (f : β → α → G) (s : Set β) (b : β),
  ∫ (y : α), s.indicator (fun x => f x y) b ∂μ = s.indicator (fun x => ∫ (y : α), f x y ∂μ) b
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_of_ge_of_lt : ∀ {n : ℕ} {i j k : Fin n}, i ≤ k → k < j → ∀ [inst : NeZero n], (i.cycleIcc j) k = k + 1
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_biUnion : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] {ι : Type u_6} {I : Set ι},
  I.Finite → ∀ {s : ι → Set E}, Bornology.IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, Bornology.IsVonNBounded 𝕜 (s i)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀AddMonoidHom.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddZeroClass (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)],
  DirectLimit.map₀AddMonoidHom f = { toFun := fun x => DirectLimit.map₀ f x, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A subset of a topological space is homeomorphic to its image under a homeomorphism.
 -/
Homeomorph.image : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → (e : X ≃ₜ Y) → (s : Set X) → ↑s ≃ₜ ↑(⇑e '' s)
-- Mathlib.Algebra.Module.Hom
AddMonoidHom.smulLeft_apply : ∀ {M : Type u_3} {A : Type u_4} [inst : AddMonoid A] [inst_1 : DistribSMul M A] (c : M),
  ⇑(AddMonoidHom.smulLeft c) = fun x => c • x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {combined : ℕ} [inst_2 : SizeOf α]
  {lw rw : ℕ} (lhs : aig.RefVec lw) (rhs : aig.RefVec rw) (h : combined = rw + lw),
  sizeOf { lw := lw, rw := rw, lhs := lhs, rhs := rhs, h := h } =
    1 + sizeOf lw + sizeOf rw + sizeOf lhs + sizeOf rhs + sizeOf h
-- Std.Http.Data.URI.Encoding
/-- Creates an `EncodedQueryString` from a `ByteArray`, panicking if the byte array is invalid.
 -/
Std.Http.URI.EncodedQueryString.ofByteArray! : ByteArray → (r : optParam (UInt8 → Bool) Std.Http.Internal.Char.isQueryChar) → Std.Http.URI.EncodedQueryString r
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.pointwiseScalarSemiring : {α : Type u₁} → {β : Type u₂} → [inst : Semiring β] → SMul (α → β) (α →₀ β)
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.HasIdealSupport.smul_mem : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} [P.HasIdealSupport] (x : R) {a : R},
  a ∈ P → -a ∈ P → x * a ∈ P
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvectorUnitary_col_eq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian) (j : n), (↑hA.eigenvectorUnitary).col j = (hA.eigenvectorBasis j).ofLp
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Mixin for a `VectorPrebundle` stating that coordinate changes are `C^n`.  -/
VectorPrebundle.IsContMDiff : {𝕜 : Type u_1} →
  {B : Type u_2} →
    {F : Type u_4} →
      {E : B → Type u_6} →
        [inst : NontriviallyNormedField 𝕜] →
          {EB : Type u_7} →
            [inst_1 : NormedAddCommGroup EB] →
              [inst_2 : NormedSpace 𝕜 EB] →
                {HB : Type u_8} →
                  [inst_3 : TopologicalSpace HB] →
                    ModelWithCorners 𝕜 EB HB →
                      [inst_4 : TopologicalSpace B] →
                        [ChartedSpace HB B] →
                          [inst_6 : (x : B) → AddCommMonoid (E x)] →
                            [inst_7 : (x : B) → Module 𝕜 (E x)] →
                              [inst_8 : NormedAddCommGroup F] →
                                [inst_9 : NormedSpace 𝕜 F] →
                                  [inst_10 : (x : B) → TopologicalSpace (E x)] →
                                    VectorPrebundle 𝕜 F E → WithTop ℕ∞ → Prop
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_two_mul_le : ∀ (n : ℕ), (2 * n).factorial ≤ (2 * n) ^ n * n.factorial
-- Mathlib.Data.Finset.Sort
Finset.sort.congr_simp : ∀ {α : Type u_1} (s s_1 : Finset α),
  s = s_1 →
    ∀ (r r_1 : α → α → Prop) (e_r : r = r_1) {inst : DecidableRel r} [inst_1 : DecidableRel r_1] [inst_2 : IsTrans α r]
      [inst_3 : Std.Antisymm r] [inst_4 : Std.Total r], s.sort r = s_1.sort r_1
-- Std.Time.Internal.UnitVal
Std.Time.Internal.instDecidableLeUnitVal : {z : ℚ} → {x y : Std.Time.Internal.UnitVal z} → Decidable (x ≤ y)
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.card_succ_choose_two_lt_card_subsetSum_of_pos : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A : Finset M} [inst_2 : LinearOrder M]
  [IsOrderedCancelAddMonoid M], (∀ x ∈ A, 0 < x) → (A.card + 1).choose 2 < A.subsetSum.card
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeFun : CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization (Type u)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ringHomComp_mul : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  (χ φ : MulChar R R') (f : R' →+* R''), (χ * φ).ringHomComp f = χ.ringHomComp f * φ.ringHomComp f
-- Mathlib.Algebra.Order.Module.Defs
Prod.instPosSMulReflectLE : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Preorder γ] [inst_4 : SMul α β] [inst_5 : SMul α γ] [PosSMulReflectLE α β] [PosSMulReflectLE α γ],
  PosSMulReflectLE α (β × γ)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- **Tower property of the conditional expectation**.

Taking the `m₂`-conditional expectation then the `m₁`-conditional expectation, where `m₁` is a
smaller σ-algebra, is the same as taking the `m₁`-conditional expectation directly.  -/
MeasureTheory.condExp_condExp_of_le : ∀ {α : Type u_1} {E : Type u_3} {f : α → E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  {m₁ m₂ m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  m₁ ≤ m₂ → ∀ (hm₂ : m₂ ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim hm₂)], μ[μ[f | m₂] | m₁] =ᵐ[μ] μ[f | m₁]
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- The unique diffeomorphism between two empty types  -/
Diffeomorph.empty : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_5} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_9} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {n : WithTop ℕ∞} →
                        {M' : Type u_13} →
                          [inst_6 : TopologicalSpace M'] →
                            [inst_7 : ChartedSpace H M'] → [IsEmpty M] → [IsEmpty M'] → Diffeomorph I I M M' n
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Left left-multiplication by row stochastic preserves `ℓ₁ norm`  -/
Matrix.vecMul_dotProduct_one_eq_one_rowStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R} {x : n → R},
  M ∈ Matrix.rowStochastic R n → x ⬝ᵥ 1 = 1 → Matrix.vecMul x M ⬝ᵥ 1 = 1
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.coe_re_inner_self_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ (x : E), ↑(RCLike.re (inner 𝕜 x (T x))) = inner 𝕜 x (T x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.negMap_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.negMap ⟦P⟧ = ⟦W'.neg P⟧
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.whiskerLeft_comp : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (Q : CategoryTheory.LocalizedMonoidal L W ε) {X Y Z : CategoryTheory.LocalizedMonoidal L W ε} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q f)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q g)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.ext_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X.PartialMap Y),
  f = g ↔ ∃ (e : f.domain = g.domain), f.hom = CategoryTheory.CategoryStruct.comp (X.isoOfEq e).hom g.hom
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.algebra : {p : ℕ} → [hp : Fact (Nat.Prime p)] → Algebra ℤ_[p] ℚ_[p]
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_lt_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {n : σ} {f : MvPolynomial σ R} {d : ℕ},
  0 < d → (MvPolynomial.degreeOf n f < d ↔ ∀ m ∈ f.support, m n < d)
-- Mathlib.CategoryTheory.Adhesive.Basic
/-- A category is adhesive if it has pushouts and pullbacks along monomorphisms,
and such pushouts are van Kampen.  -/
CategoryTheory.Adhesive : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_base : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (X : F.CoGrothendieck),
  (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id X.base
-- Aesop.Tree.Data
Aesop.RappId.instHashable : Hashable Aesop.RappId
-- Mathlib.CategoryTheory.Category.Cat.Op
CategoryTheory.Cat.opFunctor_map : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y), CategoryTheory.Cat.opFunctor.map F = F.toFunctor.op.toCatHom
-- Mathlib.Analysis.Complex.Liouville
/-- **Liouville's theorem**: a complex differentiable bounded function `f : E → F` is a constant.  -/
Differentiable.apply_eq_apply_of_bounded : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F},
  Differentiable ℂ f → Bornology.IsBounded (Set.range f) → ∀ (z w : E), f z = f w
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Module.Free.finsupp : ∀ (R : Type u_1) (M : Type u_2) (ι : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M], Module.Free R (ι →₀ M)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
ContinuousLinearMap.toSesqForm_apply_norm_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_4} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] {f : E →L[𝕜] E'} {v : E'},
  ‖(ContinuousLinearMap.toSesqForm f) v‖ ≤ ‖f‖ * ‖v‖
-- Mathlib.Data.Option.NAry
/-- Symmetric statement to `Option.map_map₂_distrib_right`.  -/
Option.map_map₂_right_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} {β' : Type u_6}
  {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f a (g b) = g' (f' a b)) → Option.map₂ f a (Option.map g b) = Option.map g' (Option.map₂ f' a b)
-- Mathlib.Data.Nat.Init
/-- A type class for natural numbers which are greater than or equal to `2`.

`NeZero` and `AtLeastTwo` are used for numeric literals, and also for groups of related lemmas
sharing a common value of `n` that needs to be nonzero, or at least `2`, and where it is
convenient to pass this information implicitly. Instances for these classes cover some of the
cases where it is most structurally obvious from the syntactic form of `n` that it satisfies the
required conditions, such as `m + 1`. Less widely used cases may be defined as lemmas rather than
global instances and then made into instances locally where needed. If implicit arguments,
appearing before other explicit arguments, are allowed to be `autoParam`s in a future version of
Lean, such an `autoParam` that is proved `by lia` might be a more general replacement for the
use of typeclass inference for this purpose.  -/
Nat.AtLeastTwo : ℕ → Prop
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.of_vadd_left : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t : Finset β},
  (s +ᵥ t).Nonempty → s.Nonempty
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_prodComm : ∀ (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂],
  (AffineEquiv.prodComm k P₁ P₂).linear = LinearEquiv.prodComm k V₁ V₂