mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (a₁ a₂ a₃ : ℤ) (h : a₁ + a₂ = a₃) (b₁ b₂ b₃ : ℤ) (h₁ : a₁ + b₁ = 0) (h₂ : a₂ + b₂ = 0) (h₃ : a₃ + b₃ = 0),
  (CategoryTheory.shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor Cᵒᵖ a₂).map
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₁ b₁ h₁).hom.app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₂ b₂ h₂).hom.app
          ((CategoryTheory.shiftFunctor C b₁).op.obj X))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op
          ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₃ b₃ h₃).inv.app X)))
-- Lean.Parser.Types
Lean.Parser.FirstTokens.seq : Lean.Parser.FirstTokens → Lean.Parser.FirstTokens → Lean.Parser.FirstTokens
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.prod.map_epi : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Epi f] [CategoryTheory.Epi g]
  [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct W X] [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct Y Z],
  CategoryTheory.Epi (CategoryTheory.Limits.prod.map f g)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialToCosimplicialAugmented_map_left : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ}
  (f : X ⟶ Y), ((CategoryTheory.simplicialToCosimplicialAugmented C).map f).left = f.unop.right.op
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_map : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [LawfulBEq α] {f : α → β → γ} {k : α},
  m.WF → Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.map f m) k = Option.map (f k) (Std.DHashMap.Raw.Const.get? m k)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.AuxGluingStruct.mk : {A : Type} →
  [inst : MetricSpace A] →
    (Space : Type) →
      (metric : MetricSpace Space) → (embed : A → Space) → Isometry embed → GromovHausdorff.AuxGluingStruct A
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.sub.match_3.eq_3 : ∀ (motive : ONote → ONote → Sort u_1) (e₁ : ONote) (n₁ : ℕ+) (a₁ e₂ : ONote) (n₂ : ℕ+) (a₂ : ONote)
  (h_1 : (x : ONote) → motive ONote.zero x) (h_2 : (o : ONote) → motive o ONote.zero)
  (h_3 :
    (o₁ e₁ : ONote) →
      (n₁ : ℕ+) →
        (a₁ : ONote) →
          o₁ = e₁.oadd n₁ a₁ → (e₂ : ONote) → (n₂ : ℕ+) → (a₂ : ONote) → motive (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)),
  (match e₁.oadd n₁ a₁, e₂.oadd n₂ a₂ with
    | ONote.zero, x => h_1 x
    | o, ONote.zero => h_2 o
    | o₁@h:(e₁.oadd n₁ a₁), e₂.oadd n₂ a₂ => h_3 o₁ e₁ n₁ a₁ h e₂ n₂ a₂) =
    h_3 (e₁.oadd n₁ a₁) e₁ n₁ a₁ ⋯ e₂ n₂ a₂
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associatorNatIsoMiddle_hom_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d) (X : b ⟶ c),
  (CategoryTheory.Bicategory.associatorNatIsoMiddle f h).hom.app X = (CategoryTheory.Bicategory.associator f X h).hom
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_iInf_dom : ∀ {α : Type ua} {β : Type ub} {ι : Sort u_1} {f : α → β} {u₁ : ι → UniformSpace α} {u₂ : UniformSpace β} {i : ι},
  UniformContinuous f → UniformContinuous f
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.functoriality_faithful`. -/
CategoryTheory.Limits.Cocones.functoriality_faithful : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) [G.Faithful], (CategoryTheory.Limits.Cocone.functoriality F G).Faithful
-- Init.Data.List.Lemmas
List.foldl_reverse : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : β → α → β} {b : β},
  List.foldl f b l.reverse = List.foldr (fun x y => f y x) b l
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mk'_toSubmonoid : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R}
  (ha : ↑sa = s), (Subring.mk' s sm sa hm ha).toSubmonoid = sm
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.add : Mathlib.Tactic.Linarith.CompSource → Mathlib.Tactic.Linarith.CompSource → Mathlib.Tactic.Linarith.CompSource
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.lhs : Lean.Meta.Grind.Arith.CommRing.DiseqCnstr → Lean.Expr
-- Mathlib.SetTheory.ZFC.Basic
/-- The empty ZFC set  -/
ZFSet.empty : ZFSet.{u_1}
-- Mathlib.CategoryTheory.Sites.Sieves
/-- If `R` is a sieve, then the `CategoryTheory.Presieve.functorPullback` of `R` is actually a sieve.
 -/
CategoryTheory.Sieve.functorPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → {X : C} → CategoryTheory.Sieve (F.obj X) → CategoryTheory.Sieve X
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.congr_tmul : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] [inst_13 : AddCommMonoid Q]
  [inst_14 : Module R Q] (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (m : M) (n : N),
  (TensorProduct.AlgebraTensorModule.congr f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.exists_constructibleSetData_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)}, (∃ S, S.toSet = s) ↔ Topology.IsConstructible s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The sup of the directions of two affine subspaces is less than or equal to the direction of
their sup.  -/
AffineSubspace.sup_direction_le : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s₁ s₂ : AffineSubspace k P), s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The identity map is a continuous additive isomorphism.  -/
ContinuousAddEquiv.refl : (M : Type u_1) → [inst : TopologicalSpace M] → [inst_1 : Add M] → M ≃ₜ+ M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.foldl_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} {δ : Type w} [Std.TransCmp cmp]
  {f : δ → (a : α) → β a → δ} {init : δ}, t₁.Equiv t₂ → Std.DTreeMap.foldl f init t₁ = Std.DTreeMap.foldl f init t₂
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Iic_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Iic a)), Subtype.val '' Set.Ioi b = Set.Ioc (↑b) a
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.equivUnitsAffineMap_symm_apply_invFun : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁), (AffineEquiv.equivUnitsAffineMap.symm u).invFun a = ↑u⁻¹ a
-- Mathlib.LinearAlgebra.Multilinear.Basis
/-- The elements of the basis are the maps which scale `b' ii.2` by the
product of all the `ii.1 ·` coordinates along `b i`.  -/
Basis.multilinearMap_apply_apply : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {M : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {κ : ι → Type u_5} (b : (i : ι) → Module.Basis (κ i) R (M i)) {ι' : Type u_6}
  {N : Type u_7} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (b' : Module.Basis ι' R N) [inst_5 : Fintype ι]
  [inst_6 : ∀ (i : ι), Finite (κ i)] (ii : ((i : ι) → κ i) × ι') (v : (i : ι) → M i),
  ((Basis.multilinearMap b b') ii) v = (∏ i, ((b i).repr (v i)) (ii.1 i)) • b' ii.2
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.card_mul_card : ∀ {G : Type u_1} [inst : AddGroup G] {S T : Set G},
  AddSubgroup.IsComplement S T → Nat.card ↑S * Nat.card ↑T = Nat.card G
-- Mathlib.Topology.Order
TopologicalSpace.GenerateOpen.below.inter : ∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → TopologicalSpace.GenerateOpen g a → Prop} (s t : Set α)
  (a : TopologicalSpace.GenerateOpen g s) (a_1 : TopologicalSpace.GenerateOpen g t),
  TopologicalSpace.GenerateOpen.below a →
    motive s a → TopologicalSpace.GenerateOpen.below a_1 → motive t a_1 → TopologicalSpace.GenerateOpen.below ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- An element `a : α` is `AddLECancellable` if `x ↦ a + x` is order-reflecting.
We will make a separate version of many lemmas that require `[MulLeftReflectLE α]` with
`AddLECancellable` assumptions instead. These lemmas can then be instantiated to specific types,
like `ENNReal`, where we can replace the assumption `AddLECancellable x` by `x ≠ ∞`.  -/
AddLECancellable : {α : Type u_1} → [Add α] → [LE α] → α → Prop
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_eq_factorial_smul_sum : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (k : ℕ),
  (⇑Polynomial.derivative)^[k] p =
    k.factorial •
      ∑ x ∈ ((⇑Polynomial.derivative)^[k] p).support,
        Polynomial.C ((x + k).choose k • p.coeff (x + k)) * Polynomial.X ^ x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instBEqCanonArgKey : BEq Lean.Meta.Grind.CanonArgKey
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.nilRankAux_le : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ι' : Type u_6} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ι'] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ι'] [inst_9 : Module.Free R M] [inst_10 : Module.Finite R M] [Nontrivial R]
  (b : Module.Basis ι R L) (b' : Module.Basis ι' R L), φ.nilRankAux b ≤ φ.nilRankAux b'
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_monomial : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {d : σ →₀ ℕ} (c : R)
  [inst_1 : Decidable (c = 0)], m.degree ((MvPolynomial.monomial d) c) = if c = 0 then 0 else d
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_map : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N : LieSubmodule R L M),
  ↑(LieSubmodule.map f N) = ⇑f '' ↑N
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.aeval_eq_prod_aroots_of_monic : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {A : Type u_2} [inst_1 : CommRing A] [inst_2 : IsDomain A]
  [inst_3 : Algebra R A],
  (Polynomial.map (algebraMap R A) f).Splits →
    f.Monic → ∀ (x : A), (Polynomial.aeval x) f = (Multiset.map (fun x_1 => x - x_1) (f.aroots A)).prod
-- Init.Data.Option.Lemmas
Option.map_guard : ∀ {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : α → β} {x : α},
  Option.map f (Option.guard p x) = if p x = true then some (f x) else none
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_eq_zero_iff_eq_zero_or_isRoot_eq_bot : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.trans_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : AddCommMonoid C] [inst_4 : Module R A] [inst_5 : Module R B]
  [inst_6 : Module R C] [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C]
  (e₁₂ : A ≃ₗc[R] B) (e₂₃ : B ≃ₗc[R] C) (x : A), (e₁₂.trans e₂₃) x = e₂₃ (e₁₂ x)
-- Lean.ProjFns
/-- Auxiliary parent projection created when a parent structure cannot be represented as a subobject
(e.g., due to diamond inheritance). Unlike regular projections, these construct the parent value
from individual fields rather than extracting a single field.
Example: `AddMonoid'.toAddZero'` when `AddZero'` cannot be a subobject of `AddMonoid'`.
 -/
Lean.AuxParentProjectionInfo : Type
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_finite_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] [Finite β]
  {t : β → Set α}, MeasureTheory.IntegrableOn f (⋃ i, t i) μ ↔ ∀ (i : β), MeasureTheory.IntegrableOn f (t i) μ
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasEigenvalue_sub_iff : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ ρ : R}, (f - ρ • LinearMap.id).HasEigenvalue μ ↔ f.HasEigenvalue (μ + ρ)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_v_desc_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain F K (-1)) (β : G ⟶ K)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
  (p q : ℤ) (h : p + -1 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q h)
      ((CochainComplex.mappingCone.desc φ α β eq).f q) =
    α.v p q h
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.ofIntSeq.congr_simp : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (seq seq_1 : ℕ → ℤ) (e_seq : seq = seq_1)
  (h : IsCauSeq (padicNorm p) fun n => ↑(seq n)), PadicInt.ofIntSeq seq h = PadicInt.ofIntSeq seq_1 ⋯
-- Mathlib.GroupTheory.Subgroup.Simple
IsSimpleGroup.instIsSimpleOrderSubgroup : ∀ {C : Type u_3} [inst : CommGroup C] [IsSimpleGroup C], IsSimpleOrder (Subgroup C)
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.mk.sizeOf_spec : ∀ (len : ℕ), sizeOf { len := len } = 1 + sizeOf len
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.termι_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- Function between 1-morphisms as a functor.  -/
CategoryTheory.PrelaxFunctor.mapFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.PrelaxFunctor B C) → (a b : B) → CategoryTheory.Functor (a ⟶ b) (F.obj a ⟶ F.obj b)
-- Mathlib.Data.Matrix.Basic
AlgEquiv.mapMatrix_trans : ∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [inst : Fintype m]
  [inst_1 : DecidableEq m] [inst_2 : CommSemiring R] [inst_3 : Semiring α] [inst_4 : Semiring β] [inst_5 : Semiring γ]
  [inst_6 : Algebra R α] [inst_7 : Algebra R β] [inst_8 : Algebra R γ] (f : α ≃ₐ[R] β) (g : β ≃ₐ[R] γ),
  f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
CategoryTheory.yonedaRingObj_map_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R : C} [inst_3 : CategoryTheory.RingObj R] {X Y : Cᵒᵖ} (f : X ⟶ Y)
  (x : Opposite.unop X ⟶ R),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yonedaRingObj R).map f)) x =
    CategoryTheory.CategoryStruct.comp f.unop x
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => RingHom.QuasiFinite
-- Mathlib.RingTheory.IsTensorProduct
/-- (Implementation): Use the more linear `IsTensorProduct.assoc`.  -/
_private.Mathlib.RingTheory.IsTensorProduct.0.IsTensorProduct.assocAux : {R : Type u_9} →
  {S : Type u_10} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {M₁ : Type u_11} →
            {M₂ : Type u_12} →
              {M₃ : Type u_13} →
                {M₁₂ : Type u_14} →
                  {M₂₃ : Type u_15} →
                    [inst_3 : AddCommMonoid M₁] →
                      [inst_4 : AddCommMonoid M₂] →
                        [inst_5 : AddCommMonoid M₃] →
                          [inst_6 : AddCommMonoid M₁₂] →
                            [inst_7 : AddCommMonoid M₂₃] →
                              [inst_8 : Module R M₁] →
                                [inst_9 : Module R M₂] →
                                  [inst_10 : Module S M₂] →
                                    [inst_11 : IsScalarTower R S M₂] →
                                      [inst_12 : Module R M₃] →
                                        [inst_13 : Module S M₃] →
                                          [IsScalarTower R S M₃] →
                                            [inst_15 : Module R M₁₂] →
                                              [inst_16 : Module S M₁₂] →
                                                [inst_17 : IsScalarTower R S M₁₂] →
                                                  [inst_18 : Module R M₂₃] →
                                                    [inst_19 : Module S M₂₃] →
                                                      [IsScalarTower R S M₂₃] →
                                                        (f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂) →
                                                          IsTensorProduct (LinearMap.restrictScalars₁₂ R R f) →
                                                            (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) →
                                                              IsTensorProduct g →
                                                                TensorProduct S M₁₂ M₃ ≃ₗ[R] TensorProduct R M₁ M₂₃
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
List.aestronglyMeasurable_sum : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : AddMonoid M]
  [inst_1 : TopologicalSpace M] [ContinuousAdd M] (l : List (α → M)),
  (∀ f ∈ l, MeasureTheory.AEStronglyMeasurable f μ) → MeasureTheory.AEStronglyMeasurable l.sum μ
-- Lean.Elab.Tactic.Grind.Basic
/-- Lifts a `SymM` computation into `GrindTacticM`.  -/
Lean.Elab.Tactic.Grind.liftSymM : {α : Type} → Lean.Meta.Sym.SymM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.isWellOrderContinuous : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (self : CategoryTheory.TransfiniteCompositionOfShape J f), self.F.IsWellOrderContinuous
-- Mathlib.Logic.Relation
Relation.SymmGen.swap : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.SymmGen r b a → Relation.SymmGen (Function.swap r) a b
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.param.sizeOf_spec : ∀ (a : Lean.IR.IRType), sizeOf (Lean.IR.LocalContextEntry.param a) = 1 + sizeOf a
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The second part of the third simplicial identity  -/
SimplexCategory.δ_comp_σ_succ_assoc : ∀ {n : ℕ} {i : Fin (n + 1)} {Z : SimplexCategory} (h : { len := n } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) h) =
    h
-- Mathlib.Data.Complex.BigOperators
Complex.ofReal_prod : ∀ {α : Type u_1} (s : Finset α) (f : α → ℝ), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.NumberTheory.Zsqrtd.ToReal
Zsqrtd.toReal_injective : ∀ {d : ℤ} (h0d : 0 ≤ d), (∀ (n : ℤ), d ≠ n * n) → Function.Injective ⇑(Zsqrtd.toReal h0d)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.CotangentSpace.map_toComp_injective : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  Function.Injective ⇑(LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
-- Init.Meta.Defs
Lean.Syntax.instReprTSyntax.repr : {ks : Lean.SyntaxNodeKinds} → Lean.TSyntax ks → ℕ → Std.Format
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_union : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {fallback : β},
  Std.DTreeMap.Internal.Impl.Const.getD (m₁.union m₂ ⋯ ⋯) k fallback =
    Std.DTreeMap.Internal.Impl.Const.getD m₂ k (Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback)
-- Init.Data.Array.Lemmas
Array.any_congr : ∀ {α : Type u_1} {start₁ start₂ stop₁ stop₂ : ℕ} {xs ys : Array α},
  xs = ys →
    ∀ {p q : α → Bool},
      (∀ (a : α), p a = q a) → start₁ = start₂ → stop₁ = stop₂ → xs.any p start₁ stop₁ = ys.any q start₂ stop₂
-- Lean.CoreM
Lean.Core.Context.mk : String →
  Lean.FileMap →
    Lean.Options →
      ℕ →
        ℕ →
          Lean.Syntax →
            Lean.Name →
              List Lean.OpenDecl →
                ℕ →
                  ℕ →
                    Lean.Name →
                      Lean.MacroScope → Bool → Option IO.CancelToken → Bool → Std.HashSet Lean.Name → Lean.Core.Context
-- Mathlib.Tactic.GCongr.Core
/-- The discharger for main goals.  -/
Mathlib.Tactic.GCongr.Context.mainGoalDischarger : Mathlib.Tactic.GCongr.Context → Lean.MVarId → Lean.MetaM Bool
-- Lean.Meta.Transform
Lean.TransformStep.continue.sizeOf_spec : ∀ (e? : optParam (Option Lean.Expr) none), sizeOf (Lean.TransformStep.continue e?) = 1 + sizeOf e?
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Squares between right adjoints can be composed "vertically" by pasting.  -/
CategoryTheory.Bicategory.rightAdjointSquare.vcomp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d e f : B} →
      {g₁ : a ⟶ c} →
        {g₂ : c ⟶ e} →
          {h₁ : b ⟶ d} →
            {h₂ : d ⟶ f} →
              {r₁ : b ⟶ a} →
                {r₂ : d ⟶ c} →
                  {r₃ : f ⟶ e} →
                    (CategoryTheory.CategoryStruct.comp r₁ g₁ ⟶ CategoryTheory.CategoryStruct.comp h₁ r₂) →
                      (CategoryTheory.CategoryStruct.comp r₂ g₂ ⟶ CategoryTheory.CategoryStruct.comp h₂ r₃) →
                        (CategoryTheory.CategoryStruct.comp r₁ (CategoryTheory.CategoryStruct.comp g₁ g₂) ⟶
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h₁ h₂) r₃)
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.ofEq_functor : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {F : CategoryTheory.Functor C₁ C₂} (hW : W₁ = W₂.inverseImage F),
  (CategoryTheory.LocalizerMorphism.ofEq hW).functor = F
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceAdd : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.BoundedVariation
/-- A real function into a finite-dimensional real vector space with bounded variation
is differentiable almost everywhere.  -/
LocallyBoundedVariationOn.ae_differentiableAt : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {f : ℝ → V},
  LocallyBoundedVariationOn f Set.univ → ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x