mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.trans_p₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P P' : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasPullback P.p₁ P'.p₀],
  (P.trans P').p₀ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst P.p₁ P'.p₀) P.p₀
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_sInf : ∀ {M : Type u_2} [inst : Add M] (S : Set (AddSubsemigroup M)), (sInf S).op = sInf (AddSubsemigroup.unop ⁻¹' S)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Given `Submonoid`s `s`, `t` of `Monoid`s `M`, `N` respectively, `s × t` as a `Submonoid` of
`M × N`.  -/
Submonoid.prod : {N : Type u_2} →
  [inst : MulOneClass N] → {M : Type u_5} → [inst_1 : MulOneClass M] → Submonoid M → Submonoid N → Submonoid (M × N)
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.piCongrRight.eq_1 : ∀ {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [inst : (j : η) → Mul (Ms j)]
  [inst_1 : (j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j),
  MulEquiv.piCongrRight es =
    { toFun := fun x j => (es j) (x j), invFun := fun x j => (es j).symm (x j), left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.subset : ∀ {α : Type u_1} {M : Matroid α} {I J : Set α}, M.Indep J → I ⊆ J → M.Indep I
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- An orthonormal basis is a Hilbert basis.  -/
OrthonormalBasis.toHilbertBasis : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [CompleteSpace E] → [inst_4 : Fintype ι] → OrthonormalBasis ι 𝕜 E → HilbertBasis ι 𝕜 E
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- The injection into a pi group at different indices commutes.

For injections of commuting elements at the same index, see `Commute.map`  -/
Pi.mulSingle_commute : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → MulOneClass (f i)],
  Pairwise fun i j => ∀ (x : f i) (y : f j), Commute (Pi.mulSingle i x) (Pi.mulSingle j y)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- If `f : M → N` is a monoid homomorphism, then `MonoidAlgebra.mapDomain f` is an algebra
homomorphism between their monoid algebras.  -/
MonoidAlgebra.mapDomainAlgHom : (R : Type u_1) →
  (A : Type u_4) →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Monoid M] → [inst_4 : Monoid N] → (M →* N) → MonoidAlgebra A M →ₐ[R] MonoidAlgebra A N
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.shiftIso.congr_simp : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (self : CategoryTheory.SingleFunctors C D A) (n a a' : A) (ha' : n + a = a'),
  self.shiftIso n a a' ha' = self.shiftIso n a a' ha'
-- Mathlib.Algebra.Group.Semiconj.Units
AddSemiconjBy.addUnits_val : ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : AddUnits M}, AddSemiconjBy a x y → AddSemiconjBy ↑a ↑x ↑y
-- Mathlib.Order.Filter.Defs
Filter.instBot : {α : Type u_1} → Bot (Filter α)
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.instInhabitedDef : {a : Type} → Inhabited (Lean.KeyedDeclsAttribute.Def a)
-- Mathlib.Analysis.Convex.LinearIsometry
/-- A vector subspace of a strict convex space is a strict convex space.

This instance has priority 900
to make sure that instances like `LinearIsometry.strictConvexSpace_range`
are tried before this one.  -/
Submodule.instStrictConvexSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] [StrictConvexSpace 𝕜 E] (p : Submodule 𝕜 E), StrictConvexSpace 𝕜 ↥p
-- Mathlib.Order.Hom.Bounded
BotHom.coe_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : SemilatticeInf β] [inst_2 : OrderBot β] (f g : BotHom α β),
  ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.IsIso HomotopicalAlgebra.CofibrantObject.HoCat.adj.counit
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.DoIfView.mk.inj : ∀ {ref optIdent cond thenBranch elseBranch ref_1 optIdent_1 cond_1 thenBranch_1 elseBranch_1 : Lean.Syntax},
  { ref := ref, optIdent := optIdent, cond := cond, thenBranch := thenBranch, elseBranch := elseBranch } =
      { ref := ref_1, optIdent := optIdent_1, cond := cond_1, thenBranch := thenBranch_1, elseBranch := elseBranch_1 } →
    ref = ref_1 ∧ optIdent = optIdent_1 ∧ cond = cond_1 ∧ thenBranch = thenBranch_1 ∧ elseBranch = elseBranch_1
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- The map `fract` with codomain restricted to `fundamentalDomain`.  -/
ZSpan.fractRestrict : {E : Type u_1} →
  {ι : Type u_2} →
    {K : Type u_3} →
      [inst : NormedField K] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace K E] →
            (b : Module.Basis ι K E) →
              [inst_3 : LinearOrder K] →
                [IsStrictOrderedRing K] → [FloorRing K] → [Fintype ι] → E → ↑(ZSpan.fundamentalDomain b)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.mapPairIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C}
  (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.left })
  (g :
    F.obj { as := CategoryTheory.Limits.WalkingPair.right } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.right })
  (X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.Limits.mapPairIso f g).hom.app X =
    (match X with
      | { as := CategoryTheory.Limits.WalkingPair.left } => f
      | { as := CategoryTheory.Limits.WalkingPair.right } => g).hom
-- Mathlib.Data.ZMod.QuotientGroup
AddAction.minimalPeriod_eq_card : ∀ {α : Type u_3} {β : Type u_4} [inst : AddGroup α] (a : α) [inst_1 : AddAction α β] (b : β)
  [inst_2 : Fintype ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b)],
  Function.minimalPeriod (fun x => a +ᵥ x) b = Fintype.card ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_add : ∀ {x y : ℝ}, x * y < 1 → Real.arctan x + Real.arctan y = Real.arctan ((x + y) / (1 - x * y))
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.δ_naturality : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂)
  (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j),
  CategoryTheory.CategoryStruct.comp (hS₁.δ i j hij) (HomologicalComplex.homologyMap φ.τ₁ j) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ.τ₃ i) (hS₂.δ i j hij)
-- Mathlib.Util.Export
Lean.Export.instInhabitedEntry : Inhabited Lean.Export.Entry
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
_private.Mathlib.CategoryTheory.Limits.Shapes.Countable.0.CategoryTheory.Limits.IsCofiltered.hasCofilteredCountableLimits_of_hasSequentialLimits : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C] →
      ProofWanted
        (∀ (J : Type) [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J]
          [CategoryTheory.CountableCategory J], CategoryTheory.Limits.HasLimitsOfShape J C)
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.usize : Lean.IR.CtorInfo → ℕ
-- Qq.Macro
Qq.Impl.instMonadLiftQuoteMUnquoteM : MonadLift Qq.Impl.QuoteM Qq.Impl.UnquoteM
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag_eq_diag2n_prod : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i₀ : ι) (D : ι → F)
  (hD : (Matrix.diagonal D).det = 1),
  ⟨Matrix.diagonal D, hD⟩ =
    {i | i ≠ i₀}.noncommProd (fun i => if hi : i ≠ i₀ then Matrix.SpecialLinearGroup.diag2n hi (D i) ⋯ else 1) ⋯
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.opensRange_awayι : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  AlgebraicGeometry.Scheme.Hom.opensRange (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) =
    AlgebraicGeometry.Proj.basicOpen 𝒜 f
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_continuous : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸], Continuous NormedSpace.exp
-- Mathlib.Data.Multiset.MapFold
Multiset.card_map : ∀ {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α), (Multiset.map f s).card = s.card
-- Lean.Parser.Types
Lean.Parser.FirstTokens.tokens : List Lean.Parser.Token → Lean.Parser.FirstTokens
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_zsmul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddGroup α] [inst_1 : StarAddMonoid α] (c : ℤ) (M : Matrix m n α),
  (c • M).conjTranspose = c • M.conjTranspose
-- Mathlib.CategoryTheory.Join.Basic
/-- One can exchange `mapWhiskerLeft` and `mapWhiskerRight`.  -/
CategoryTheory.Join.mapWhisker_exchange : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (Fₗ Gₗ : CategoryTheory.Functor C E)
  (Fᵣ Gᵣ : CategoryTheory.Functor D E') (αₗ : Fₗ ⟶ Gₗ) (αᵣ : Fᵣ ⟶ Gᵣ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapWhiskerLeft Fₗ αᵣ)
      (CategoryTheory.Join.mapWhiskerRight αₗ Gᵣ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapWhiskerRight αₗ Fᵣ)
      (CategoryTheory.Join.mapWhiskerLeft Gₗ αᵣ)
-- Init.Data.SInt.Lemmas
Int64.ofNat_bitVecToNat : ∀ (n : BitVec 64), Int64.ofNat n.toNat = Int64.ofBitVec n
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.coe_inv' : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  (A : ↥(Matrix.symplecticGroup l R)), ↑A⁻¹ = (↑A)⁻¹
-- Mathlib.Analysis.Normed.Group.Int
Int.norm_eq_abs : ∀ (n : ℤ), ‖n‖ = |↑n|
-- Mathlib.Data.Finset.NoncommProd
Multiset.map_noncommSum : ∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : AddMonoid α] [inst_1 : AddMonoid β] [inst_2 : FunLike F α β]
  [inst_3 : AddMonoidHomClass F α β] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise AddCommute) (f : F),
  f (s.noncommSum comm) = (Multiset.map (⇑f) s).noncommSum ⋯
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_lt_pow_iff_norm_le_pow_sub_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (n : ℤ), ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)
-- Mathlib.Topology.Algebra.InfiniteSum.Module
Summable.smul_const : ∀ {ι : Type u_5} {R : Type u_7} {M : Type u_9} [inst : Semiring R] [inst_1 : TopologicalSpace R]
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [ContinuousSMul R M] {f : ι → R}
  {L : SummationFilter ι}, Summable f L → ∀ (a : M), Summable (fun z => f z • a) L
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- The underlying map of `pullbackDiagonalIso`  -/
CategoryTheory.Limits.pullbackDiagonalMapIso.hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
        {U V₁ V₂ : C} →
          (f : X ⟶ Y) →
            (i : U ⟶ Y) →
              (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) →
                (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) →
                  [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂] →
                    CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal f)
                        (CategoryTheory.Limits.pullback.map
                          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
                          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
                          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
                          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯) ⟶
                      CategoryTheory.Limits.pullback i₁ i₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.deriv_arcsin : deriv Real.arcsin = fun x => 1 / √(1 - x ^ 2)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.State.result? : Lean.Meta.SynthInstance.State → Option Lean.Meta.AbstractMVarsResult
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The orthogonal complement of the closure of a submodule (as a `ClosedSubmodule`) is equal to
the orthogonal complement.  -/
ClosedSubmodule.orthogonal_closure' : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), K.closureᗮ = { toSubmodule := Kᗮ, isClosed' := ⋯ }
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.isoMk_inv_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreOneHypercover.isoMk._auto_1)
  (w₁₁ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (h₀ i).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_3)
  (w₁₂ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (h₀ j).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_5)
  {i j : F.I₀} (k : F.I₁ i j),
  (CategoryTheory.PreOneHypercover.isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).inv.h₁ k =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ k).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (h₁ (s₁.symm ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) k))).inv)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instInhabited : {R : Type u_1} → {a b : R} → [Zero R] → Inhabited (QuadraticAlgebra R a b)
-- Aesop.Search.Expansion.Norm
Aesop.NormStep.runPreSimpRules : Aesop.UnorderedArraySet Lean.MVarId → Aesop.NormStep
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.map_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (op : β → γ) (f : α → β),
  Filter.Germ.map op ↑f = ↑(op ∘ f)
-- Mathlib.Topology.Homeomorph.Defs
/-- Precomposing by a homeomorphism does not change the image of the interior of a preimage.  -/
image_interior_preimage_comp : ∀ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X → Y),
  IsHomeomorph e → ∀ (f : Y → Z) (s : Set Z), f ∘ e '' interior (f ∘ e ⁻¹' s) = f '' interior (f ⁻¹' s)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
isBigO_deriv_rpow_const_atTop : ∀ (p : ℝ), (deriv fun x => x ^ p) =O[Filter.atTop] fun x => x ^ (p - 1)
-- Mathlib.Algebra.WithConv
/-- `WithConv.ofConv` and `WithConv.toConv` as an equivalence.  -/
WithConv.equiv : (A : Type u_2) → WithConv A ≃ A
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instDefinableOfDefinable₂ : (f : ZFSet.{u_1} → ZFSet.{u_1} → ZFSet.{u_1}) →
  [ZFSet.Definable₂ f] →
    (n : ℕ) →
      (g₁ g₂ : (Fin n → ZFSet.{u_1}) → ZFSet.{u_1}) →
        [ZFSet.Definable n g₁] → [ZFSet.Definable n g₂] → ZFSet.Definable n fun s => f (g₁ s) (g₂ s)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `e` has already been internalized.  -/
Lean.Meta.Grind.alreadyInternalized : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SMul.smul_stabilizer_def : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] (s : Set α) (g : ↥(MulAction.stabilizer G s))
  (x : ↑s), ↑(g • x) = ↑g • ↑x
-- Init.Data.SInt.Basic
/-- Converts 8-bit signed integers to 32-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.toInt32 : Int8 → Int32
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionList.mk.inj : ∀ {isIncomplete : Bool} {items : Array Lean.Lsp.CompletionItem} {isIncomplete_1 : Bool}
  {items_1 : Array Lean.Lsp.CompletionItem},
  { isIncomplete := isIncomplete, items := items } = { isIncomplete := isIncomplete_1, items := items_1 } →
    isIncomplete = isIncomplete_1 ∧ items = items_1
-- Mathlib.Topology.Sheaves.Alexandrov
/-- Given a structured arrow `f` with domain `U : Opens X` over `principals X`,
this functor sends `f` to its "generator", an element of `X`.  -/
Alexandrov.generator : {X : Type v} →
  [inst : TopologicalSpace X] →
    [inst_1 : Preorder X] →
      [inst_2 : Topology.IsUpperSet X] →
        (U : TopologicalSpace.Opens X) →
          CategoryTheory.Functor (CategoryTheory.StructuredArrow (Opposite.op U) (Alexandrov.principals X)) X
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.instInhabitedGCongrLemma : Inhabited Mathlib.Tactic.GCongr.GCongrLemma
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves limits of shape `Jᵒᵖ`, then `F : C ⥤ Dᵒᵖ` preserves colimits
of shape `J`.  -/
CategoryTheory.Limits.preservesColimitsOfShape_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ)
  [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F.leftOp], CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgEquiv.ofLeftInverse_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {g : B → A} {f : A →ₐ[R] B} (h : Function.LeftInverse g ⇑f) (x : A),
  ↑((AlgEquiv.ofLeftInverse h) x) = f x
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.IsNoetherian.toIsLocallyNoetherian : ∀ {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsNoetherian X], AlgebraicGeometry.IsLocallyNoetherian X
-- Mathlib.RingTheory.Valuation.RankOne
/-- If a valuation has rank at most one and is non trivial,
then it has rank one  -/
Valuation.RankLeOne.rankOne_of_exists : {Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] →
    {K : Type u_3} →
      [inst_1 : DivisionRing K] → (v : Valuation K Γ₀) → [v.RankLeOne] → (∃ x, x ≠ 0 ∧ v x ≠ 1) → v.RankOne
-- Mathlib.Algebra.Group.Even
even_neg : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {a : α}, Even (-a) ↔ Even a
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.intro.injEq : ∀ (x : Lean.Name) (p : Mathlib.Tactic.ITauto.Proof) (x_1 : Lean.Name) (p_1 : Mathlib.Tactic.ITauto.Proof),
  (Mathlib.Tactic.ITauto.Proof.intro x p = Mathlib.Tactic.ITauto.Proof.intro x_1 p_1) = (x = x_1 ∧ p = p_1)
-- Mathlib.Tactic.SetNotationForOrder
/-- Delaborate `x ≥ y` into `x ⊇ y` if the type is tagged with `@[use_set_notation_for_order]`.  -/
Mathlib.Meta.SetNotationForOrder.delabGe : Lean.PrettyPrinter.Delaborator.Delab
-- Init.Data.Float.Model.Float
Float.Model.mk.injEq : ∀ (toBits : UInt64) (valid : Float.Model.Format.binary64.Valid toBits.toBitVec) (toBits_1 : UInt64)
  (valid_1 : Float.Model.Format.binary64.Valid toBits_1.toBitVec),
  ({ toBits := toBits, valid := valid } = { toBits := toBits_1, valid := valid_1 }) = (toBits = toBits_1)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.π₃_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), CategoryTheory.ShortComplex.π₃.map f = f.τ₃
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.preinclusion_map₂ : ∀ {B : Type u} [inst : Quiver B] {a b : B} (f g : CategoryTheory.Discrete (Quiver.Path a b)) (η : f ⟶ g),
  (CategoryTheory.FreeBicategory.preinclusion B).map₂ η = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Order.AddTorsor
instIsCancelVAddOfIsOrderedCancelVAdd : ∀ {G : Type u_1} {P : Type u_2} [inst : PartialOrder G] [inst_1 : PartialOrder P] [inst_2 : VAdd G P]
  [IsOrderedCancelVAdd G P], IsCancelVAdd G P
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonWaitForILeansParams.toJson : Lean.Lsp.WaitForILeansParams → Lean.Json
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.normalizedMooreComplex_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
  (AlgebraicTopology.normalizedMooreComplex C).map f = AlgebraicTopology.NormalizedMooreComplex.map f
-- Std.Data.HashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.HashMap.getKeyD : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → α → α
-- Mathlib.GroupTheory.IsSubnormal
/-- A subnormal additive subgroup is either the whole group or it is contained in a
proper normal additive subgroup.  -/
AddSubgroup.IsSubnormal.lt_normal : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.IsSubnormal → H = ⊤ ∨ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.mk.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' ι'} [inst_6 : Algebra S S']
  (val val_1 : ι → P'.Ring) (e_val : val = val_1)
  (aeval_val : ∀ (i : ι), (MvPolynomial.aeval P'.val) (val i) = (algebraMap S S') (P.val i)),
  { val := val, aeval_val := aeval_val } = { val := val_1, aeval_val := ⋯ }
-- Mathlib.Control.Traversable.Basic
/-- The function on objects defined by an `ApplicativeTransformation`.  -/
ApplicativeTransformation.app : {F : Type u → Type v} →
  [inst : Applicative F] →
    {G : Type u → Type w} → [inst_1 : Applicative G] → ApplicativeTransformation F G → (α : Type u) → F α → G α
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_nsmul : ∀ {α : Type u} [inst : AddMonoid α] (a : α) (n : ℕ), ↑(n • a) = n • ↑a
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.zsmul_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (b : ℤ) (v : Π₀ (i : ι), β i) (i : ι),
  (b • v) i = b • v i
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.Products.isGood_nil : ∀ {I : Type u_1} [inst : LinearOrder I],
  Profinite.NobelingProof.Products.isGood {fun x => false} Profinite.NobelingProof.Products.nil
-- Lean.Parser.Command
Lean.Parser.Command.declBody.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.mapBilinear_apply : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂),
  ((TensorProduct.mapBilinear σ₁₂ M N M₂ N₂) f) g = TensorProduct.map f g