mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite.eq_1 : ∀ {M N : ProfiniteAddGrp.{u}},
  ProfiniteAddGrp.instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite =
    { coe := fun f => ⇑(ProfiniteAddGrp.Hom.hom f) }
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.instSubsingletonOfForall : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Subsingleton (V → W)], Subsingleton (G.Copy H)
-- Mathlib.CategoryTheory.Idempotents.Biproducts
/-- A formal direct factor `P : Karoubi C` of an object `P.X : C` in a
preadditive category is actually a direct factor of the image `(toKaroubi C).obj P.X`
of `P.X` in the category `Karoubi C`  -/
CategoryTheory.Idempotents.Karoubi.decomposition : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (P : CategoryTheory.Idempotents.Karoubi C) → P ⊞ P.complement ≅ (CategoryTheory.Idempotents.toKaroubi C).obj P.X
-- Mathlib.Algebra.Notation.Prod
Prod.snd_add : ∀ {M : Type u_8} {N : Type u_9} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).2 = p.2 + q.2
-- Mathlib.Data.Set.Finite.Basic
/-- `Finset α` is order isomorphic to the type of finite sets in `α`.  -/
OrderIso.finsetSetFinite : {α : Type u} → Finset α ≃o { s // s.Finite }
-- Lean.Data.JsonRpc
Lean.JsonRpc.Request.id : {α : Type u} → Lean.JsonRpc.Request α → Lean.JsonRpc.RequestID
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject C),
  HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans.app X =
    HomotopicalAlgebra.CofibrantObject.toHoCat.map
      { hom := HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj (HomotopicalAlgebra.CofibrantObject.ι.obj X) }
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_iff_continuousOn_differentiableOn : ∀ {𝕜 : 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 : ℕ∞},
  UniqueDiffOn 𝕜 s →
    (ContDiffOn 𝕜 (↑n) f s ↔
      (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
        ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.sumCongr_apply : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H') (a : V ⊕ W),
  (f.sumCongr g) a = Sum.map (⇑f) (⇑g) a
-- Aesop.Rule.Name
Aesop.BuilderName.destruct : Aesop.BuilderName
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
CategoryTheory.Limits.limitSubobjectProduct_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor J C),
  CategoryTheory.Mono (CategoryTheory.Limits.limitSubobjectProduct F)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap.eq_1 : ∀ {α : Type u} {β : Type v} (x_2 : (a : α) → none = some a → β), Std.Internal.List.Option.dmap✝ none x_2 = none
-- Init.Data.String.Basic
String.Pos.Raw.utf8PrevAux_lt_of_pos : ∀ (cs : List Char) (i p : String.Pos.Raw), i < p → p ≠ 0 → (String.Pos.Raw.utf8PrevAux cs i p).byteIdx < p.byteIdx
-- Mathlib.Algebra.Star.CentroidHom
CentroidHom.star_centerToCentroidCenter : ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] [inst_1 : StarRing α] (z : ↥(NonUnitalStarSubsemiring.center α)),
  star (CentroidHom.centerToCentroidCenter z) = CentroidHom.centerToCentroidCenter (star z)
-- Mathlib.Algebra.Free
FreeAddSemigroup.instInhabited.eq_1 : ∀ {α : Type u} [inst : Inhabited α], FreeAddSemigroup.instInhabited = { default := FreeAddSemigroup.of default }
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
/-- Cochains of degree `n` from `(singleFunctor C p).obj X` to `K` identify
to `X ⟶ K.X q` when `p + n = q`.  -/
CochainComplex.HomComplex.Cochain.fromSingleEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X : C} →
          {K : CochainComplex C ℤ} →
            {p q n : ℤ} →
              p + n = q →
                CochainComplex.HomComplex.Cochain ((CochainComplex.singleFunctor C p).obj X) K n ≃+ (X ⟶ K.X q)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_le_one : ∀ (x : ℝ), x.sigmoid ≤ 1
-- Mathlib.LinearAlgebra.Complex.Module
Commute.realPart_imaginaryPart : ∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [inst_1 : StarRing A] [inst_2 : Module ℂ A] [IsScalarTower ℂ A A]
  [SMulCommClass ℂ A A] [inst_5 : StarModule ℂ A] (x : A) [IsStarNormal x], Commute ↑(realPart x) ↑(imaginaryPart x)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.eraseMin.eq_1 : ∀ {α : Type u_1}, Ordnode.nil.eraseMin = Ordnode.nil
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {X₁ X₂ X₃ : C} {f : X₁ ⟶ X₂} {g : X₂ ⟶ X₃}
  {zero : autoParam (CategoryTheory.CategoryStruct.comp f g = 0) CategoryTheory.ShortComplex.zero._autoParam}
  {X₁_1 X₂_1 X₃_1 : C} {f_1 : X₁_1 ⟶ X₂_1} {g_1 : X₂_1 ⟶ X₃_1}
  {zero_1 : autoParam (CategoryTheory.CategoryStruct.comp f_1 g_1 = 0) CategoryTheory.ShortComplex.zero._autoParam},
  { X₁ := X₁, X₂ := X₂, X₃ := X₃, f := f, g := g, zero := zero } =
      { X₁ := X₁_1, X₂ := X₂_1, X₃ := X₃_1, f := f_1, g := g_1, zero := zero_1 } →
    X₁ = X₁_1 ∧ X₂ = X₂_1 ∧ X₃ = X₃_1 ∧ f ≍ f_1 ∧ g ≍ g_1
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.mkNatCastInst : Lean.Meta.Grind.Arith.FieldNormNum.M✝ Lean.Expr
-- Init.Meta
Lean.termEval_prio_ : Lean.ParserDescr
-- Mathlib.Order.RelIso.Basic
RelEmbedding.trichotomous : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [Std.Trichotomous s],
  Std.Trichotomous r
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, panicking if no such pair exists.
 -/
Std.ExtTreeMap.getEntryLE! : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtTreeMap α β cmp → α → α × β
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.LawfulOperator.lt_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [Std.Sat.AIG.LawfulOperator α β f]
  (entry : Std.Sat.AIG.Entrypoint α) (input : β entry.aig), entry.ref.gate < (f entry.aig input).aig.decls.size
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.IterM.take.surjective_of_zero_lt : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (it : Std.IterM m β),
  0 < it.internalState.countdown → ∃ it₀ k, it = Std.IterM.take k it₀
-- Mathlib.Tactic.Tauto
/-- Calls `distribNotAt` on the head of `state.fvars` up to `nIters` times, returning
early on failure.
 -/
Mathlib.Tactic.Tauto.distribNotAt : ℕ → Mathlib.Tactic.Tauto.DistribNotState → Lean.MetaM Mathlib.Tactic.Tauto.DistribNotState
-- Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
ModularFormClass.modularForm.congr_simp : ∀ {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : FunLike F UpperHalfPlane ℂ]
  [inst_1 : ModularFormClass F Γ k] (f f_1 : F),
  f = f_1 → ModularFormClass.modularForm f = ModularFormClass.modularForm f_1
-- Mathlib.Dynamics.Minimal
denseRange_smul : ∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [MulAction.IsMinimal M α] (x : α), DenseRange fun c => c • x
-- Init.Data.Vector.Count
Vector.countP_push_of_neg : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α} {xs : Vector α n},
  ¬p a = true → Vector.countP p (xs.push a) = Vector.countP p xs
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.serreDerivative_sub : ∀ (k : ℂ) (F G : UpperHalfPlane → ℂ),
  MDiff F →
    MDiff G → Derivative.serreDerivative k (F - G) = Derivative.serreDerivative k F - Derivative.serreDerivative k G
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
ContinuousOn.angle_sign_comp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → Real.Angle} {s : Set α},
  ContinuousOn f s → (∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑Real.pi) → ContinuousOn (Real.Angle.sign ∘ f) s
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeUniv : {α : Type u} → [Fintype α] → Fintype ↑Set.univ
-- Mathlib.Data.Finset.Functor
Finset.commApplicative : ∀ [inst : (P : Prop) → Decidable P], CommApplicative Finset
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- If a map `f : X → Y` is continuous on every compact subset of `X` then it is continuous when
viewed as a map from `CompactCoherentification X` to `CompactCoherentification Y`.  -/
CompactCoherentification.continuous_map_of_continuousOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  (∀ (K : Set X), IsCompact K → ContinuousOn f K) → Continuous (CompactCoherentification.map f)
-- Init.Core
Sigma.mk.injEq : ∀ {α : Type u} {β : α → Type v} (fst : α) (snd : β fst) (fst_1 : α) (snd_1 : β fst_1),
  (⟨fst, snd⟩ = ⟨fst_1, snd_1⟩) = (fst = fst_1 ∧ snd ≍ snd_1)
-- Batteries.Recycling.RBTree.Lemmas
/-- A "representable cut" is one generated by `cmp a` for some `a`. This is always a valid cut.  -/
RBTree.RBNode.instIsStrictCut : ∀ {α : Type u_1} (cmp : α → α → Ordering) (a : α), RBTree.RBNode.IsStrictCut cmp (cmp a)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.addSemigroup : {𝕜 : 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] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : AddSemigroup G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [ContMDiffAdd I' n G] → AddSemigroup (ContMDiffMap I I' N G n)
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaKey.expr : Lean.Meta.Sym.AlphaKey → Lean.Expr
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorMapObj_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J) {X₁ : CategoryTheory.GradedObject I₁ C₁}
  {X₂ : CategoryTheory.GradedObject I₂ C₂} {X₃ : CategoryTheory.GradedObject I₃ C₃} {Y : C₄} (j : J)
  [inst_4 : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  {φ φ' : CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y},
  (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
          φ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
          φ') →
    φ = φ'
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l l_1 : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_2 r : Std.DTreeMap.Internal.Impl α β) →
                    l_1 = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r))
                          h)
  (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β)
  (x_2 : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false),
  x = Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf →
    x_1 ≍ x_2 →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
        | Std.DTreeMap.Internal.Impl.inner size k v l l_1@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r),
          h_3 => h_2 size k v l l_1 size_1 k_1 v_1 l_2 r h h_3) ≍
        h_1 size k v l x_2
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
_private.Mathlib.Data.QPF.Multivariate.Constructions.Cofix.0.MvQPF.Cofix.bisim_aux : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n}
  (r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop),
  (∀ (x : MvQPF.Cofix F α), r x x) →
    (∀ (x y : MvQPF.Cofix F α),
        r x y → MvFunctor.map (TypeVec.id ::: Quot.mk r) x.dest = MvFunctor.map (TypeVec.id ::: Quot.mk r) y.dest) →
      ∀ (x y : MvQPF.Cofix F α), r x y → x = y
-- Mathlib.Data.List.Sort
/-- The list obtained from a strictly antitone tuple is sorted.  -/
StrictAnti.sortedGT_ofFn : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, StrictAnti f → (List.ofFn f).SortedGT
-- Init.Data.Format.Basic
/-- Creates a group in which as few `Format.line`s as possible are rendered as newlines.

This is an alias for `Format.group`, with `FlattenBehavior` set to `fill`.
 -/
Std.Format.fill : Std.Format → Std.Format
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- Help the typechecker by converting a point in a topological space to a
point in the fundamental groupoid of that space.  -/
FundamentalGroupoid.fromTop : {X : TopCat} → ↑X → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj X)
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extended_one : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N),
  FractionalIdeal.extended L hf 1 = 1
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instAdditiveCochainComplexIntQ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Q.Additive
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₁₃_obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₃) {X Y : C₂}
  (g : X ⟶ Y) (X_1 : C₁), ((F.flip₁₃.obj G).map g).app X_1 = ((F.obj X_1).map g).app G
-- Mathlib.RingTheory.Extension.Generators
/-- The backwards direction of the canonical isomorphism `T ⊗[R] R[Xᵢ] ≃ₐ[T] T[Xᵢ]` as
a map of extensions.  -/
Algebra.Generators.baseChangeToBaseChange : {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 ι) →
              (T : Type u_2) →
                [inst_3 : CommRing T] →
                  [inst_4 : Algebra R T] → (Algebra.Generators.baseChange T P).toExtension.Hom P.toExtension.baseChange
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.uAssignment : Lean.Meta.Sym.UnifyM.State✝ → Array (Option Lean.Level)
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Raw.toArray_iter : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → m.iter.toArray = m.toArray
-- Mathlib.LinearAlgebra.Matrix.Basis
basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix : ∀ {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_9} [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M) (c : Module.Basis κ R N) (c' : Module.Basis κ' R N)
  (f : M →ₗ[R] N) [inst_5 : Fintype ι'] [inst_6 : Finite κ] [inst_7 : Fintype ι] [inst_8 : Fintype κ']
  [inst_9 : DecidableEq ι] [inst_10 : DecidableEq ι'],
  c.toMatrix ⇑c' * (LinearMap.toMatrix b' c') f * b'.toMatrix ⇑b = (LinearMap.toMatrix b c) f
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.val_inv_unit : ∀ {M : Type u_6} [inst : Monoid M] {x : M} (hx : IsOfFinOrder x), ↑hx.unit⁻¹ = x ^ (orderOf x - 1)
-- Mathlib.Data.Stream.Init
Stream'.corec_id_f_eq_iterate : ∀ {α : Type u} (f : α → α) (a : α), Stream'.corec id f a = Stream'.iterate f a
-- Mathlib.Order.Category.DistLat
/-- The underlying `LatticeHom`.  -/
DistLat.Hom.hom' : {X Y : DistLat} → X.Hom Y → LatticeHom ↑X ↑Y
-- Init.Data.List.Zip
_private.Init.Data.List.Zip.0.List.getElem?_zipWithAll.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (h_1 : Unit → motive none none)
  (h_2 : (a? : Option α) → (b? : Option β) → motive a? b?),
  (match none, none with
    | none, none => h_1 ()
    | a?, b? => h_2 a? b?) =
    h_1 ()
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- **Alias** of `PowerSeries.weierstrassMod_zero_left`. -/
PowerSeries.zero_weierstrassMod : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (g : PowerSeries A)
  [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A], 0 %ʷ g = 0
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- The difference `f m₁ - f m₂` is controlled in terms of `‖f‖` and `‖m₁ - m₂‖`,
less precise version.
For a more precise but less usable version, see `norm_image_sub_le'`.
The bound is `‖f m - f m'‖ ≤ ‖f‖ * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1)`.  -/
ContinuousAlternatingMap.norm_image_sub_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F) (m₁ m₂ : ι → E),
  ‖f m₁ - f m₂‖ ≤ ‖f‖ * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Except.map.match_1.eq_1 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (err : ε) (h_1 : (err : ε) → motive (Except.error err))
  (h_2 : (v : α) → motive (Except.ok v)),
  (match Except.error err with
    | Except.error err => h_1 err
    | Except.ok v => h_2 v) =
    h_1 err
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- Closure of a subgroup `K` equals `K`.  -/
Subgroup.closure_eq : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G), Subgroup.closure ↑K = K
-- Mathlib.Order.SuccPred.Relation
/-- **Alias** of `transGen_of_succ_of_refl`.

---

`(n, m)` is in the transitive closure of a reflexive relation `~` if `i ~ succ i` and
`succ i ~ i` for all `i` between `n` and `m`.  -/
transGen_of_succ_of_reflexive : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] (r : α → α → Prop) {n m : α}
  [Std.Refl r],
  (∀ i ∈ Set.Ico n m, r i (Order.succ i)) → (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → Relation.TransGen r n m
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- Pullback of a normed add torsor along an injective map.  -/
Function.Injective.normedAddTorsor : {V : Type u_2} →
  {P : Type u_3} →
    [inst : SeminormedAddCommGroup V] →
      [inst_1 : PseudoMetricSpace P] →
        [inst_2 : NormedAddTorsor V P] →
          {Q : Type u_6} →
            [inst_3 : VAdd V Q] →
              [inst_4 : VSub V Q] →
                [Nonempty Q] →
                  [inst_6 : PseudoMetricSpace Q] →
                    (f : Q → P) →
                      Function.Injective f →
                        (∀ (c : V) (x : Q), f (c +ᵥ x) = c +ᵥ f x) →
                          (∀ (x y : Q), x -ᵥ y = f x -ᵥ f y) →
                            (∀ (x y : Q), dist x y = dist (f x) (f y)) → NormedAddTorsor V Q
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, n ≠ 0 → n < Function.minimalPeriod f x → ¬Function.IsPeriodicPt f n x
-- Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
MeasureTheory.exists_nat_measurableEquiv_range_coe_fin_of_finite : ∀ (α : Type u_1) [inst : MeasurableSpace α] [StandardBorelSpace α] [Finite α],
  ∃ n, Nonempty (α ≃ᵐ ↑(Set.range fun x => ↑↑x))
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.map_nsmul : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N) (n : ℕ) (a : M),
  f (n • a) = n • f a
-- Mathlib.Data.Real.Sign
Real.sign_apply_eq : ∀ (r : ℝ), r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1
-- Lean.Level
Lean.instReprLevelMVarId : Repr Lean.LevelMVarId
-- Mathlib.Data.Num.Lemmas
PosNum.one_le_cast : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] (n : PosNum), 1 ≤ ↑n
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.mk : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {f₀ f₁ : C(X, Y)} →
          (toContinuousMap : C(↑unitInterval × X, Y)) →
            (∀ (x : X), toContinuousMap.toFun (0, x) = f₀ x) →
              (∀ (x : X), toContinuousMap.toFun (1, x) = f₁ x) → f₀.Homotopy f₁