mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecificLimits.Normed
/-- Partial sums of an alternating antitone series with an odd number of terms provide
upper bounds on the limit.  -/
Antitone.tendsto_le_alternating_series : ∀ {E : Type u_4} [inst : Ring E] [inst_1 : PartialOrder E] [IsOrderedRing E] [inst_3 : TopologicalSpace E]
  [OrderClosedTopology E] {l : E} {f : ℕ → E},
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l) →
    Antitone f → ∀ (k : ℕ), l ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.brecOn.eq : ∀ {motive : FBinopElab.Tree✝ → Sort u} (t : FBinopElab.Tree✝)
  (F_1 : (t : FBinopElab.Tree✝) → FBinopElab.Tree.below✝ t → motive t),
  FBinopElab.Tree.brecOn✝ t F_1 = F_1 t (FBinopElab.Tree.brecOn.go✝ t F_1).2
-- Mathlib.NumberTheory.LucasPrimality
/-- A number `p` is prime if and only if there exists an `a` such that
`a^(p-1) = 1 mod p` and `a^((p-1)/q) ≠ 1 mod p` for all prime factors `q` of `p-1`.
 -/
lucas_primality_iff : ∀ (p : ℕ), Nat.Prime p ↔ ∃ a, a ^ (p - 1) = 1 ∧ ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
LinearMap.restrictScalarsRange₂.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7}
  {P' : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : SMul S R] [inst_3 : AddCommMonoid M]
  [inst_4 : Module R M] [inst_5 : AddCommMonoid N] [inst_6 : Module R N] [inst_7 : AddCommMonoid P]
  [inst_8 : Module R P] [inst_9 : Module S M] [inst_10 : Module S N] [inst_11 : Module S P]
  [inst_12 : IsScalarTower S R M] [inst_13 : IsScalarTower S R N] [inst_14 : IsScalarTower S R P]
  [inst_15 : AddCommMonoid M'] [inst_16 : Module S M'] [inst_17 : AddCommMonoid N'] [inst_18 : Module S N']
  [inst_19 : AddCommMonoid P'] [inst_20 : Module S P'] [inst_21 : SMulCommClass R S P] (i i_1 : M' →ₗ[S] M)
  (e_i : i = i_1) (j j_1 : N' →ₗ[S] N) (e_j : j = j_1) (k k_1 : P' →ₗ[S] P) (e_k : k = k_1) (hk : Function.Injective ⇑k)
  (B B_1 : M →ₗ[R] N →ₗ[R] P) (e_B : B = B_1) (hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range),
  i.restrictScalarsRange₂ j k hk B hB = i_1.restrictScalarsRange₂ j_1 k_1 ⋯ B_1 ⋯
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
IsUltrametricDist.invariantExtension.congr_simp : ∀ (K : Type u_1) [inst : NormedField K] (L : Type u_2) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K],
  IsUltrametricDist.invariantExtension K L = IsUltrametricDist.invariantExtension K L
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addZ_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P → W.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → W.addZ P Q = (P 0 * Q 2 - Q 0 * P 2) ^ 3 / (P 2 * Q 2)
-- Mathlib.FieldTheory.SeparableDegree
/-- If `E / F` is a finite extension, then its separable degree is equal to its degree if and
only if it is a separable extension.  -/
Field.finSepDegree_eq_finrank_iff : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E],
  Field.finSepDegree F E = Module.finrank F E ↔ Algebra.IsSeparable F E
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
/-- Specialization of `exists_primeSpectrum_prod_le_and_ne_bot_of_domain` to Dedekind domains:
Let `I : Ideal A` be a nonzero ideal, where `A` is a Dedekind domain that is not a field.
Then `exists_primeSpectrum_prod_le_and_ne_bot_of_domain` states we can find a product of prime
ideals that is contained within `I`. This lemma extends that result by making the product minimal:
let `M` be a maximal ideal that contains `I`, then the product including `M` is contained within `I`
and the product excluding `M` is not contained within `I`.  -/
PrimeSpectrum.exists_multiset_prod_cons_le_and_prod_not_le : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A],
  ¬IsField A →
    ∀ {I M : Ideal A},
      I ≠ ⊥ →
        I ≤ M →
          ∀ [hM : M.IsMaximal],
            ∃ Z,
              (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedSymbolTag.default : Lean.Lsp.SymbolTag
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGT_distinguished : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  (t.triangleLEGT n).obj X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Std.Data.HashMap.Lemmas
Std.HashMap.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} (h : k ∈ Std.HashMap.filterMap f m),
  (f (m.getKey k ⋯) m[k]).isSome = true
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_congr_ae : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [inst_1 : TopologicalSpace ε] {f g : α → ε}, f =ᵐ[μ] g → (MeasureTheory.MemLp f p μ ↔ MeasureTheory.MemLp g p μ)
-- Lean.Parser.Command
Lean.Parser.Command.axiom.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
MeasurableEmbedding.prodMk_right : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_3} {γ : Type u_4} [MeasurableSingletonClass α]
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : γ → β},
  MeasurableEmbedding f → ∀ (x : α), MeasurableEmbedding fun y => (f y, x)
-- Mathlib.Topology.Separation.Basic
instR1SpaceProd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [R1Space X] [inst_2 : TopologicalSpace Y] [R1Space Y],
  R1Space (X × Y)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
Differentiable.fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₂ : E → F × G},
  Differentiable 𝕜 f₂ → Differentiable 𝕜 fun x => (f₂ x).1
-- Lean.Elab.SetOption
Lean.Elab.checkDeprecatedOption : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadOptions m] → [Lean.MonadLog m] → [Lean.AddMessageContext m] → Lean.Name → Lean.OptionDecl → m Unit
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_eq_some_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k k' : α}, m.get? k = some k' ↔ ∃ (h : k ∈ m), m.get k h = k'
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_dvd_gcd_mul_right_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n k : α), gcd m n ∣ gcd m (n * k)
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetsExtEntry.local : Lean.Widget.WidgetInstance → Lean.Widget.PanelWidgetsExtEntry
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.convexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E}
  {f : E → β}, StrictConvexOn 𝕜 s f → ConvexOn 𝕜 s f
-- Init.Data.Dyadic.Basic
/-- The dyadic number `0`.  -/
Dyadic.zero : Dyadic
-- Std.Data.HashMap.Iterator
/-- Returns a finite iterator over the entries of a hash map.
The iterator yields the elements of the map in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.HashMap.Raw.iter : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → Std.Iter (α × β)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.spanCarrier.below.of : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)}
  {motive : (a : Projectivization K V) → Projectivization.Subspace.spanCarrier S a → Prop} (x : Projectivization K V)
  (hx : x ∈ S), Projectivization.Subspace.spanCarrier.below ⋯
-- Mathlib.Topology.Order.LeftRightNhds
/-- The following statements are equivalent:

0. `s` is a neighborhood of `a` within `[a, +∞)`;
1. `s` is a neighborhood of `a` within `[a, b]`;
2. `s` is a neighborhood of `a` within `[a, b)`;
3. `s` includes `[a, u)` for some `u ∈ (a, b]`;
4. `s` includes `[a, u)` for some `u > a`.
 -/
TFAE_mem_nhdsGE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a b : α},
  a < b →
    ∀ (s : Set α),
      [s ∈ nhdsWithin a (Set.Ici a), s ∈ nhdsWithin a (Set.Icc a b), s ∈ nhdsWithin a (Set.Ico a b),
          ∃ u ∈ Set.Ioc a b, Set.Ico a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s].TFAE
-- Mathlib.Algebra.Group.Center
/-- Conditions for an element to be multiplicatively central  -/
IsMulCentral : {M : Type u_1} → [Mul M] → M → Prop
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- A functor from `ComposableArrows ι 1` to the pretriangulated category.  -/
CategoryTheory.Triangulated.SpectralObject.ω₁ : {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.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  CategoryTheory.Triangulated.SpectralObject C ι →
                    CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C
-- Init.Data.SInt.Lemmas
Int16.toBitVec_mul : ∀ {a b : Int16}, (a * b).toBitVec = a.toBitVec * b.toBitVec
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instVAdd : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_3} →
      {M : Type u_5} → [inst_1 : TopologicalSpace M] → [inst_2 : VAdd R M] → [ContinuousConstVAdd R M] → VAdd R C(α, M)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- For every nonzero ideal `I` of `v`, there are finitely many maximal ideals `v` such that
`v^(val_v(I))`, regarded as a fractional ideal, is not `(1)`.  -/
Ideal.hasFiniteMulSupport_coe : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 →
    Function.HasFiniteMulSupport fun v => ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- Since `⦋0⦌ : SimplexCategory` is terminal, `Δ[0]` has a unique point and thus
`OneTruncation₂ ((truncation 2).obj Δ[0])` has a unique inhabitant.  -/
SSet.instUniqueOneTruncation₂DeltaZero : Unique (SSet.OneTruncation₂ ((SSet.truncation 2).obj (SSet.stdSimplex.obj { len := 0 })))
-- Mathlib.Data.Nat.Digits.Defs
/-- (Impl.) An auxiliary definition for `digits`, to help get the desired definitional unfolding.  -/
Nat.digitsAux : (b : ℕ) → 2 ≤ b → ℕ → List ℕ
-- Mathlib.Analysis.Calculus.Deriv.Star
/-- If `f` is differentiable at `conj z`, then `conj ∘ f ∘ conj` is differentiable at `z`.  -/
DifferentiableAt.conj_conj : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {x : 𝕜} [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜},
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (⇑(starRingEnd 𝕜) ∘ f ∘ ⇑(starRingEnd 𝕜)) ((starRingEnd 𝕜) x)
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.whiskerOfCompIdIsoSelf_hom_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  (t : CategoryTheory.Bicategory.LeftExtension f g),
  t.whiskerOfCompIdIsoSelf.hom.right = (CategoryTheory.Bicategory.rightUnitor t.extension).hom
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square
```
  X --inl--> X ⊞ Y
  |            |
  0           snd
  |            |
  v            v
  0 ---0-----> Y
```
is a pullback square.
 -/
CategoryTheory.IsPullback.inl_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0
-- Mathlib.Algebra.DirectSum.Ring
/-- Multiplication is associative  -/
DirectSum.GSemiring.mul_assoc : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GSemiring A] (a b c : GradedMonoid A), a * b * c = a * (b * c)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommMonoidWithZero.mk : {α : Type u_3} →
  [toCommMonoidWithZero : CommMonoidWithZero α] →
    [toLinearOrder : LinearOrder α] →
      [toPosMulStrictMono : PosMulStrictMono α] →
        [toOrderBot : OrderBot α] → [toIsBotZeroClass : IsBotZeroClass α] → LinearOrderedCommMonoidWithZero α
-- Mathlib.CategoryTheory.Category.Pairwise
/-- Composition of morphisms in `CategoryTheory.Pairwise ι`.  -/
CategoryTheory.Pairwise.comp : {ι : Type v} → {o₁ o₂ o₃ : CategoryTheory.Pairwise ι} → o₁.Hom o₂ → o₂.Hom o₃ → o₁.Hom o₃
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(X - r, g) = g(r)`  -/
Polynomial.resultant_X_sub_C_left : ∀ {R : Type u_1} [inst : CommRing R] (g : Polynomial R) (n : ℕ) (r : R),
  g.natDegree ≤ n → (Polynomial.X - Polynomial.C r).resultant g 1 n = Polynomial.eval r g
-- Batteries.Data.List.Lemmas
List.countPBefore_le_countP : ∀ {α : Type u_1} {i : ℕ} {xs : List α} (p : α → Bool), List.countPBefore p xs i ≤ List.countP p xs
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, if `A` is free and `B` is flat,
then `[B[A] : B] = [A : R]`. See also `Subalgebra.adjoin_rank_le`.  -/
Subalgebra.LinearDisjoint.adjoin_rank_eq_rank_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Free R ↥A] [Module.Flat R ↥B] [Nontrivial R] [Nontrivial S],
      Module.rank ↥B ↥(Algebra.adjoin ↥B ↑A) = Module.rank R ↥A
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- If we rewrite into this expression, then the goal will be solved.  -/
Mathlib.Tactic.ClickSuggestions.GrwInfo.rflTarget? : Mathlib.Tactic.ClickSuggestions.GrwInfo → Option Lean.Expr
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
/-- If `S` is a sub-`R`-algebra of `A` and `S` is finitely-generated as an `R`-module,
then all elements of `S` are integral over `R`.  -/
IsIntegral.of_mem_of_fg : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] (S : Subalgebra R B),
  (Subalgebra.toSubmodule S).FG → ∀ x ∈ S, IsIntegral R x
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- A smooth function `f : M → N` induces a morphism of sheaves (of rings) `𝒪_N ⟶ f_* 𝒪_M`,
by pre-composing with `f`.  -/
ContMDiff.smoothSheafCommRingHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              {IM : ModelWithCorners 𝕜 EM HM} →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          {I : ModelWithCorners 𝕜 E H} →
                            {M : Type u} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  {R : Type u} →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        {EP : Type u_7} →
                                          [inst_11 : NormedAddCommGroup EP] →
                                            [inst_12 : NormedSpace 𝕜 EP] →
                                              {HP : Type u_8} →
                                                [inst_13 : TopologicalSpace HP] →
                                                  (IP : ModelWithCorners 𝕜 EP HP) →
                                                    (P : Type u) →
                                                      [inst_14 : TopologicalSpace P] →
                                                        [inst_15 : ChartedSpace HP P] →
                                                          [inst_16 : CommRing R] →
                                                            [inst_17 : ContMDiffRing I (↑⊤) R] →
                                                              (f : M → P) →
                                                                (hf : ContMDiff IM IP (↑⊤) f) →
                                                                  smoothSheafCommRing IP I P R ⟶
                                                                    (TopCat.Sheaf.pushforward CommRingCat
                                                                          (TopCat.ofHom
                                                                            { toFun := f, continuous_toFun := ⋯ })).obj
                                                                      (smoothSheafCommRing IM I M R)
-- Mathlib.Geometry.Manifold.ContMDiffMap
ContMDiffMap.instContinuousMapClass : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {H' : Type u_5} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞},
  ContinuousMapClass (ContMDiffMap I I' M M' n) M M'
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.foldl_eq_foldl_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  {f : δ → α → β → δ} {init : δ},
  Std.DTreeMap.Raw.foldl f init t = Array.foldl (fun a b => f a b.1 b.2) init (Std.DTreeMap.Raw.Const.toArray t)
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.prevAux.go.match_1.splitter : {s : String.Slice} →
  (motive :
      (off : ℕ) →
        (h₁ : off < s.utf8ByteSize) → ¬(s.getUTF8Byte { byteIdx := off } h₁).IsUTF8FirstByte → 0 ≠ off → Sort u_1) →
    (off : ℕ) →
      (h₁ : off < s.utf8ByteSize) →
        (hbyte : ¬(s.getUTF8Byte { byteIdx := off } h₁).IsUTF8FirstByte) →
          (this : 0 ≠ off) →
            ((h₁ : 0 < s.utf8ByteSize) →
                (hbyte : ¬(s.getUTF8Byte { } h₁).IsUTF8FirstByte) → (this : 0 ≠ 0) → motive 0 h₁ hbyte this) →
              ((off : ℕ) →
                  (h₁ : off + 1 < s.utf8ByteSize) →
                    (hbyte : ¬(s.getUTF8Byte { byteIdx := off + 1 } h₁).IsUTF8FirstByte) →
                      (this : 0 ≠ off + 1) → motive off.succ h₁ hbyte this) →
                motive off h₁ hbyte this
-- Init.Data.List.Sort.Lemmas
/-- Another statement of stability of merge sort.
If a pair `[a, b]` is a sublist of `l` and `le a b`,
then `[a, b]` is still a sublist of `mergeSort le l`.
 -/
List.pair_sublist_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool} {a b : α} {l : List α},
  (∀ (a b c : α), le a b = true → le b c = true → le a c = true) →
    (∀ (a b : α), (le a b || le b a) = true) → le a b = true → [a, b].Sublist l → [a, b].Sublist (l.mergeSort le)
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.EnrichedOrdinaryCategory.mk : {V : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [toEnrichedCategory : CategoryTheory.EnrichedCategory V C] →
            (homEquiv : {X Y : C} → (X ⟶ Y) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] Y)) →
              autoParam (∀ (X : C), homEquiv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.eId V X)
                  CategoryTheory.EnrichedOrdinaryCategory.homEquiv_id._autoParam →
                autoParam
                    (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
                      homEquiv (CategoryTheory.CategoryStruct.comp f g) =
                        CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.leftUnitor
                              (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.tensorHom (homEquiv f) (homEquiv g))
                            (CategoryTheory.eComp V X Y Z)))
                    CategoryTheory.EnrichedOrdinaryCategory.homEquiv_comp._autoParam →
                  CategoryTheory.EnrichedOrdinaryCategory V C
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RcoSlice : (α : Type u_1) → [Ord α] → Type u_1
-- Mathlib.Data.Set.Prod
injective_toPullbackDiag : ∀ {X : Type u_1} {Y : Sort u_2} (f : X → Y), Function.Injective (toPullbackDiag f)
-- Init.Data.Array.Sort.Lemmas
/-- Another statement of stability of merge sort.
If `c` is a sorted sublist of `xs.toList`,
then `c` is still a sublist of `(mergeSort le xs).toList`.
 -/
Array.sublist_mergeSort : ∀ {α : Type u_1} {xs : Array α} {le : α → α → Bool},
  (∀ (a b c : α), le a b = true → le b c = true → le a c = true) →
    (∀ (a b : α), (le a b || le b a) = true) →
      ∀ {ys : List α},
        List.Pairwise (fun x1 x2 => le x1 x2 = true) ys → ys.Sublist xs.toList → ys.Sublist (xs.mergeSort le).toList
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.dropPrefix?.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((list : List α) → motive list []) →
        ((head : α) → (tail : List α) → motive [] (head :: tail)) →
          ((a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)) → motive x x_1
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.ortho_eq_sub_inner : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x : V) {y : V},
  ‖y‖ = 1 → InnerProductGeometry.ortho✝ y x = x - inner ℝ y x • y
-- Mathlib.Data.EReal.Basic
instZeroLEOneClassEReal : ZeroLEOneClass EReal
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_above_dvd : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q] [Module.Flat S T], r.ramificationIdx S ∣ r.ramificationIdx R
-- Lean.Data.PersistentHashMap
_private.Lean.Data.PersistentHashMap.0.Lean.PersistentHashMap.size_set : ∀ {α : Type u_1} {β : Type u_2} {ks : Array α} {vs : Array β},
  ks.size = vs.size →
    ∀ (i : Fin ks.size) (j : Fin vs.size) (k : α) (v : β), (ks.set (↑i) k ⋯).size = (vs.set (↑j) v ⋯).size