mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.Stonean.Basic
/-- ```
               X
               |
              (f)
               |
               \/
  Z ---(e)---> Y
```
If `Z` is a Stonean space, `f : X ⟶ Y` an epi in `Profinite` and `e : Z ⟶ Y` is arbitrary,
then `lift e f` is a fixed (but arbitrary) lift of `e` to a morphism `Z ⟶ X`. It is
`CompHaus.lift e f` as a morphism in `Profinite`.
 -/
Profinite.lift : {X Y : Profinite} →
  {Z : Stonean} → (Stonean.toProfinite.obj Z ⟶ Y) → (f : X ⟶ Y) → [CategoryTheory.Epi f] → Stonean.toProfinite.obj Z ⟶ X
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.hypValue.sizeOf_spec : ∀ (a : Lean.FVarId) (a_1 : Lean.SubExpr.Pos),
  sizeOf (Lean.SubExpr.GoalLocation.hypValue a a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Data.Array.Basic
/-- Inserts an element into an array at the specified index. Panics if the index is greater than the
size of the array.

In other words, the new element is inserted into the array `as` after the first `i` elements of
`as`.

This function takes worst case `O(n)` time because it has to swap the inserted element into place.
`Array.insertIdx` and `Array.insertIdxIfInBounds` are safer alternatives.

Examples:
 * `#["tues", "thur", "sat"].insertIdx! 1 "wed" = #["tues", "wed", "thur", "sat"]`
 * `#["tues", "thur", "sat"].insertIdx! 2 "wed" = #["tues", "thur", "wed", "sat"]`
 * `#["tues", "thur", "sat"].insertIdx! 3 "wed" = #["tues", "thur", "sat", "wed"]`
 -/
Array.insertIdx! : {α : Type u} → Array α → ℕ → α → Array α
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.summand_smul_def : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d),
  (Monoid.PushoutI.of i) g • w =
    (Monoid.PushoutI.NormalWord.equivPair i).symm
      (let __src := (Monoid.PushoutI.NormalWord.equivPair i) w;
      { head := g * ((Monoid.PushoutI.NormalWord.equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯,
        normalized := ⋯ })
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} [inst_5 : SizeOf R] [inst_6 : SizeOf M]
  [inst_7 : SizeOf N] [inst_8 : SizeOf ι] (toMultilinearMap : MultilinearMap R (fun x => M) N)
  (map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toMultilinearMap.toFun v = 0),
  sizeOf { toMultilinearMap := toMultilinearMap, map_eq_zero_of_eq' := map_eq_zero_of_eq' } =
    1 + sizeOf toMultilinearMap
-- Mathlib.Topology.UniformSpace.Basic
uniformity_eq_uniformity_interior : ∀ {α : Type ua} [inst : UniformSpace α], uniformity α = (uniformity α).lift' interior
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
/-- The image of a natural transformation between type-valued functors satisfies the universal
property of images  -/
CategoryTheory.FunctorToTypes.monoFactorisationIsImage : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {F G : CategoryTheory.Functor C (Type u)} →
      (f : F ⟶ G) → CategoryTheory.Limits.IsImage (CategoryTheory.FunctorToTypes.monoFactorisation f)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- A function `f` satisfies `IsBoundedLinearMap 𝕜 f` if it is linear and satisfies the
inequality `‖f x‖ ≤ M * ‖x‖` for some positive constant `M`.

(We put only the typeclasses strictly necessary for the definition, although the main case of
interest is when `𝕜` itself is a normed ring and `E, F` are normed modules.)  -/
IsBoundedLinearMap : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring 𝕜] →
        [inst_1 : SeminormedAddCommGroup E] →
          [Module 𝕜 E] → [inst_3 : SeminormedAddCommGroup F] → [Module 𝕜 F] → (E → F) → Prop
-- Mathlib.Order.Hom.Basic
OrderIso.toRelIsoLT.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  e.toRelIsoLT = { toEquiv := e.toEquiv, map_rel_iff' := ⋯ }
-- Mathlib.Data.Matrix.DMatrix
DMatrix.zero_apply : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [inst : (i : m) → (j : n) → Zero (α i j)] (i : m) (j : n),
  0 i j = 0
-- Mathlib.Order.Concept
Concept.compl_extent : ∀ {α : Type u_2} {r' : α → α → Prop} [IsStrictTotalOrder α r'] (c' : Concept α α r'), c'.extentᶜ = c'.intent
-- Mathlib.Topology.Connected.Basic
isConnected_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, IsConnected (connectedComponent x)
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
_private.Mathlib.Combinatorics.Enumerative.Partition.GenFun.0.Nat.Partition.aux_prod_f_eq_prod_coeff : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R) {n : ℕ}
  (p : n.Partition) {s : Finset ℕ},
  Finset.Icc 1 n ⊆ s →
    0 ∉ s →
      (Multiset.toFinsupp p.parts).prod f =
        ∏ i ∈ s,
          (PowerSeries.coeff (p.toFinsuppAntidiag i)) (1 + ∑' (j : ℕ), f i (j + 1) • PowerSeries.X ^ (i * (j + 1)))
-- Mathlib.Order.Interval.Basic
Interval.coe_iInf₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : CompleteLattice α] [inst_1 : DecidableLE α]
  (f : (i : ι) → κ i → Interval α), ↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceFrom_slice : ∀ {s : String.Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} {p : (s.slice p₁ p₂ h).Pos},
  (s.slice p₁ p₂ h).sliceFrom p = s.slice (String.Slice.Pos.ofSlice p) p₂ ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosReflectLT.toContravariantClass : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : Zero α} {inst_2 : Preorder α} [self : MulPosReflectLT α],
  ContravariantClass { x // 0 ≤ x } α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
-- Mathlib.Algebra.Order.Monoid.WithTop
WithBot.le_self_add : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [CanonicallyOrderedAdd α] {x : WithBot α},
  x ≠ ⊥ → ∀ (y : WithBot α), y ≤ y + x
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.induction_on : ∀ {R : Type u_1} [inst : Semiring R] {M : LaurentPolynomial R → Prop} (p : LaurentPolynomial R),
  (∀ (a : R), M (LaurentPolynomial.C a)) →
    (∀ {p q : LaurentPolynomial R}, M p → M q → M (p + q)) →
      (∀ (n : ℕ) (a : R),
          M (LaurentPolynomial.C a * LaurentPolynomial.T ↑n) →
            M (LaurentPolynomial.C a * LaurentPolynomial.T (↑n + 1))) →
        (∀ (n : ℕ) (a : R),
            M (LaurentPolynomial.C a * LaurentPolynomial.T (-↑n)) →
              M (LaurentPolynomial.C a * LaurentPolynomial.T (-↑n - 1))) →
          M p
-- Init.Data.BitVec.Lemmas
BitVec.toNat_udiv : ∀ {n : ℕ} {x y : BitVec n}, (x / y).toNat = x.toNat / y.toNat
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `E1` and `E2` are intermediate fields, then the `Module.finrank` of
the compositum of `E1` and `E2` is less than or equal to the product of that of `E1` and `E2`.  -/
IntermediateField.finrank_sup_le : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L), Module.finrank K ↥(E1 ⊔ E2) ≤ Module.finrank K ↥E1 * Module.finrank K ↥E2
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.comap : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M} {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (V : Submodule R N) {f : M →ₗ[R] N},
  f x ≡ f y [SMOD V] → x ≡ y [SMOD Submodule.comap f V]
-- Mathlib.GroupTheory.Finiteness
/-- In a canonically ordered and well-quasi-ordered additive monoid
(typical example is `ℕ ^ k`), any subtractive submonoid is finitely generated.  -/
AddSubmonoid.fg_of_subtractive : ∀ {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelAddMonoid M]
  [CanonicallyOrderedAdd M] {P : AddSubmonoid M}, (∀ x ∈ P, ∀ (y : M), x + y ∈ P → y ∈ P) → P.FG
-- Init.Data.Nat.ToString
Nat.digitChar_eq_e : ∀ {n : ℕ}, n.digitChar = 'e' ↔ n = 14
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.forget₂_algebra_map : ∀ {R : Type u} [inst : CommRing R] (X Y : BialgCat R) (f : X ⟶ Y),
  (CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).map f = AlgCat.ofHom ↑(BialgCat.Hom.toBialgHom f)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_isRelPrime_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {a b : M}, IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The ring homomorphism is an isometry.  -/
RingHomIsometric.norm_map : ∀ {R₁ : Type u_5} {R₂ : Type u_6} {inst : Semiring R₁} {inst_1 : Semiring R₂} {inst_2 : Norm R₁} {inst_3 : Norm R₂}
  {σ : R₁ →+* R₂} [self : RingHomIsometric σ] {x : R₁}, ‖σ x‖ = ‖x‖
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- Constructor for isomorphisms in `Pseudofunctor.DescentData`.  -/
CategoryTheory.Pseudofunctor.DescentData.isoMk : {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} →
              {D₁ D₂ : F.DescentData f} →
                (e : (i : ι) → D₁.obj i ≅ D₂.obj i) →
                  autoParam
                      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
                        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
                        CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (e i₁).hom)
                            (D₂.hom q f₁ f₂ ⋯ ⋯) =
                          CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯)
                            ((F.map f₂.op.toLoc).toFunctor.map (e i₂).hom))
                      CategoryTheory.Pseudofunctor.DescentData.isoMk._auto_1 →
                    (D₁ ≅ D₂)
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.isHamiltonian_iff_isPath_and_length_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [inst_1 : Fintype α],
  p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1
-- Init.Data.List.Nat.Modify
List.modifyTailIdx_modifyTailIdx_le : ∀ {α : Type u_1} {f g : List α → List α} (i j : ℕ) (l : List α),
  j ≤ i → (l.modifyTailIdx j f).modifyTailIdx i g = l.modifyTailIdx j fun l => (f l).modifyTailIdx (i - j) g
-- Mathlib.Order.SupClosed
latticeClosure_idem : ∀ {α : Type u_3} [inst : Lattice α] (s : Set α), latticeClosure (latticeClosure s) = latticeClosure s
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.instInhabitedAssignment : Inhabited Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ}
  {gp_n : GenContFract.Pair K},
  (GenContFract.of v).s.get? n = some gp_n →
    ∃ ifp, GenContFract.IntFractPair.stream v (n + 1) = some ifp ∧ ↑ifp.b = gp_n.b
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosReflectLE.toMulPosStrictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α] [MulPosReflectLE α], MulPosStrictMono α
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.rat_add : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (r : ℚ), LiouvilleWith p (↑r + x)
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S}
  [inst : CategoryTheory.Limits.HasPullback f g],
  P f → ∀ (x : ↥X) (y : ↥Y), f x = g y → ∃ a, (CategoryTheory.Limits.pullback.snd f g) a = y
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.conj_cong_is_cong : ∀ (g : ConjAct (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)),
  CongruenceSubgroup.IsCongruenceSubgroup Γ → CongruenceSubgroup.IsCongruenceSubgroup (g • Γ)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_lt_Iio : ∀ (o : Ordinal.{u}), (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.lift.{u + 1, u} o
-- Init.Grind.AC
Lean.Grind.AC.Seq.startsWithVar_k.eq_1 : ∀ (s : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var),
  s.startsWithVar_k x = Lean.Grind.AC.Seq.rec (fun y => Nat.beq x y) (fun y x_1 x_2 => Nat.beq x y) s
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_nonpos_of_nonpos_of_nonneg : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [MulPosMono α], a ≤ 0 → 0 ≤ b → a * b ≤ 0
-- Mathlib.Data.TypeVec
TypeVec.toSubtype'.eq_2 : ∀ (n_2 : ℕ) (α_2 : TypeVec.{u} (n_2 + 1)) (p_2 : (α_2.prod α_2).Arrow (TypeVec.repeat (n_2 + 1) Prop))
  (x_2 : { x // TypeVec.ofRepeat (p_2 Fin2.fz (TypeVec.prod.mk Fin2.fz x.1 x.2)) }),
  TypeVec.toSubtype' p_2 Fin2.fz x_2 = ⟨↑x_2, ⋯⟩
-- Init.Data.List.Basic
List.append_cons : ∀ {α : Type u} (as : List α) (b : α) (bs : List α), as ++ b :: bs = as ++ [b] ++ bs
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift₃_p₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] [inst_4 : F.Faithful] {Z : C} (x₁ : Z ⟶ A₁)
  (x₂ : Z ⟶ A₂) (x₃ : Z ⟶ A₃)
  (h₁₂ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₂) f₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₃) f₃),
  CategoryTheory.CategoryStruct.comp (hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃)
      (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃) =
    x₂
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- `haarProduct K₀` is the product of intervals `[0, (K : K₀)]`, for all compact sets `K`.
For all `U`, we can show that `prehaar K₀ U ∈ haarProduct K₀`.  -/
MeasureTheory.Measure.haar.haarProduct : {G : Type u_1} → [Group G] → [inst : TopologicalSpace G] → Set G → Set (TopologicalSpace.Compacts G → ℝ)
-- Mathlib.Logic.Encodable.Basic
/-- Invariant relationship between encoding and decoding  -/
Encodable.encodek : ∀ {α : Type u_1} [self : Encodable α] (a : α), Encodable.decode (Encodable.encode a) = some a
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.constMonoidHom.eq_1 : ∀ (α : Type u_5) (β : Type u_6) [inst : MulOneClass β],
  Pi.constMonoidHom α β = { toFun := Function.const α, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mem_top : ∀ {R : Type u} [inst : NonAssocSemiring R] (x : R), x ∈ ⊤
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.rangeKerLift.eq_1 : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H),
  QuotientGroup.rangeKerLift φ = QuotientGroup.lift φ.ker φ.rangeRestrict ⋯
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι_midπ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ) {Z : CochainComplex C ℤ}
  (h : ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.mid ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι✝ f n₀)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q) h) =
    CategoryTheory.CategoryStruct.comp
      ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.ι h
-- Mathlib.RingTheory.Localization.Basic
AlgHom.extendScalarsOfIsLocalization_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  (S : Type u_4) [inst_3 : CommSemiring S] [inst_4 : Algebra R S] (M : Submonoid R) [inst_5 : IsLocalization M S]
  [inst_6 : Algebra R A] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] [inst_9 : Algebra R B]
  [inst_10 : Algebra S B] [inst_11 : IsScalarTower R S B] (f : A →ₐ[R] B) (a : A),
  (AlgHom.extendScalarsOfIsLocalization S M f) a = f a
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.HasExplicitPullbacksOfInclusions.mk : ∀ {P : TopCat → Prop} [inst : CompHausLike.HasExplicitFiniteCoproducts P],
  (∀ {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), CompHausLike.HasExplicitPullback CategoryTheory.Limits.coprod.inl f) →
    CompHausLike.HasExplicitPullbacksOfInclusions P
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.getDiscrRange : Lean.Meta.MatcherInfo → Std.Rco ℕ
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_kernel_sum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι]
  (κ : ι → ProbabilityTheory.Kernel α β) (hκ : ∀ (i : ι), ProbabilityTheory.IsSFiniteKernel (κ i))
  (f : α → β → ENNReal),
  (ProbabilityTheory.Kernel.sum κ).withDensity f = ProbabilityTheory.Kernel.sum fun i => (κ i).withDensity f
-- Init.Data.List.Nat.Range
List.range'_eq_append_iff : ∀ {s n step : ℕ} {xs ys : List ℕ},
  List.range' s n step = xs ++ ys ↔ ∃ k ≤ n, xs = List.range' s k step ∧ ys = List.range' (s + k * step) (n - k) step
-- Init.Data.UInt.Lemmas
UInt8.toNat.eq_1 : ∀ (n : UInt8), n.toNat = n.toBitVec.toNat
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarSpaceCoord_target : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.polarSpaceCoord K).target =
    ⇑(NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K).symm ⁻¹'
      Set.univ ×ˢ Set.univ.pi fun i => Complex.polarCoord.target
-- Mathlib.Order.Filter.AtTopBot.Disjoint
Filter.disjoint_atTop_principal_Iic : ∀ {α : Type u_3} [inst : Preorder α] [NoTopOrder α] (x : α), Disjoint Filter.atTop (Filter.principal (Set.Iic x))
-- Mathlib.Order.Interval.Set.InitialSeg
Set.principalSegIio_toFun : ∀ {α : Type u_1} [inst : Preorder α] (j : α) (j_1 : ↑(Set.Iio j)), (Set.principalSegIio j).toFun j_1 = ↑j_1
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_substInv_right : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R),
  PowerSeries.constantCoeff P = 0 →
    ∀ [inst_1 : Invertible ((PowerSeries.coeff 1) P)], PowerSeries.subst P.substInv P = PowerSeries.X
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_last' : ∀ {n : ℕ} {β : Sort u_2} (x : β) (p : Fin n → β), (Fin.last n).insertNth x p = Fin.snoc p x
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instCommMonoidWithZero : {M : Type u_1} → [inst : CommMonoidWithZero M] → CommMonoidWithZero (Associates M)
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
/-- If a sequence of functions between real or complex normed spaces are differentiable on a
preconnected open set, they form a Cauchy sequence _at_ `x`, and their derivatives are Cauchy
uniformly on the set, then the functions form a Cauchy sequence at any point in the set.  -/
cauchy_map_of_uniformCauchySeqOn_fderiv : ∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] {G : Type u_4}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ι → E → G} {f' : ι → E → E →L[𝕜] G} {s : Set E},
  IsOpen s →
    IsPreconnected s →
      UniformCauchySeqOn f' l s →
        (∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y) →
          ∀ {x₀ x : E},
            x₀ ∈ s → x ∈ s → Cauchy (Filter.map (fun n => f n x₀) l) → Cauchy (Filter.map (fun n => f n x) l)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mono_enorm : ∀ {α : Type u_1} {ε : Type u_5} {ε' : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : TopologicalSpace ε'] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'},
  MeasureTheory.Integrable g μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ) → MeasureTheory.Integrable f μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany_list_equiv_foldl : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ : Std.DTreeMap.Internal.Impl α fun x => β} {l : List (α × β)}
  (h : t₁.WF),
  (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t₁ l ⋯)).Equiv
    (List.foldl (fun acc p => Std.DTreeMap.Internal.Impl.insert! p.1 p.2 acc) t₁ l)
-- Batteries.Control.Lemmas
StateT.run_tryCatch : ∀ {m : Type u_1 → Type u_2} {ε : Type u_3} {σ α : Type u_1} [inst : Monad m] [inst_1 : MonadExceptOf ε m]
  (body : StateT σ m α) (handler : ε → StateT σ m α) (s : σ),
  (tryCatch body handler).run s = tryCatch (body.run s) fun x => (handler x).run s
-- Mathlib.Algebra.Regular.Basic
IsRightRegular.left_of_commute : ∀ {R : Type u_1} [inst : Mul R] {a : R}, (∀ (b : R), Commute a b) → IsRightRegular a → IsLeftRegular a
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.comp.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} {R'' : Type u_4} {S'' : Type u_5}
  {ι'' : Type u_6} [inst_6 : CommRing R''] [inst_7 : CommRing S''] [inst_8 : Algebra R'' S'']
  {P'' : Algebra.Generators R'' S'' ι''} [inst_9 : Algebra R' R''] [inst_10 : Algebra R' S''] [inst_11 : Algebra S S']
  [inst_12 : Algebra S' S''] [inst_13 : Algebra S S''] [inst_14 : IsScalarTower R' R'' S'']
  [inst_15 : IsScalarTower R' S' S''] [inst_16 : IsScalarTower S S' S''] (f f_1 : P'.Hom P''),
  f = f_1 → ∀ (g g_1 : P.Hom P'), g = g_1 → f.comp g = f_1.comp g_1
-- Lean.Meta.ACLt
_private.Lean.Meta.ACLt.0.Lean.Meta.ACLt.main.getParamsInfo : Lean.Expr → ℕ → Lean.MetaM (Array Lean.Meta.ParamInfo)
-- Mathlib.NumberTheory.Chebyshev
Nat.lcmUpto_eq_prod_pow_log : ∀ (n : ℕ), n.lcmUpto = ∏ p ∈ n.primesLE, p ^ Nat.log p n
-- Mathlib.Order.Category.DistLat
DistLat.coe_id : ∀ {X : DistLat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- A linear isometry between two modules restricts to a linear isometry
from any submodule `p` of the domain onto the image of that submodule.

This is a version of `LinearMap.submoduleMap` extended to linear isometries.  -/
LinearIsometry.submoduleMap : {R : Type u_11} →
  {M : Type u_14} →
    {M₁ : Type u_15} →
      [inst : Ring R] →
        [inst_1 : SeminormedAddCommGroup M] →
          [inst_2 : SeminormedAddCommGroup M₁] →
            [inst_3 : Module R M] →
              [inst_4 : Module R M₁] → (p : Submodule R M) → (e : M →ₗᵢ[R] M₁) → ↥p →ₗᵢ[R] ↥(Submodule.map (↑e) p)
-- Mathlib.Order.Defs.Unbundled
Maximal.prop : ∀ {α : Type u_1} [inst : LE α] {P : α → Prop} {x : α}, Maximal P x → P x