mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F], F.mapDerivedCategory.IsTriangulated
-- Mathlib.Algebra.Module.FinitePresentation
/-- Let `M` be a finite `R`-module and `N` be a finitely presented `R`-module. If `f : M →ₗ[R] N`
is a linear map whose localization at a prime ideal `p` is bijective, then there exists
`g ∉ p` such that `f` is already bijective under the localization away from `g`.  -/
Module.FinitePresentation.exists_notMem_bijective : ∀ {R : Type u_5} {M : Type u_6} {N : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Finite R M] [Module.FinitePresentation R N] (f : M →ₗ[R] N)
  (p : Ideal R) [inst_7 : p.IsPrime] {Mₚ : Type u_3} {Nₚ : Type u_4} [inst_8 : AddCommGroup Mₚ]
  [inst_9 : AddCommGroup Nₚ] [inst_10 : Module R Mₚ] [inst_11 : Module R Nₚ] (fM : M →ₗ[R] Mₚ) (fN : N →ₗ[R] Nₚ)
  [inst_12 : IsLocalizedModule p.primeCompl fM] [inst_13 : IsLocalizedModule p.primeCompl fN],
  Function.Bijective ⇑((IsLocalizedModule.map p.primeCompl fM fN) f) →
    ∃ g ∉ p, Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers g)) f)
-- Mathlib.Data.Set.BooleanAlgebra
Set.instOrderTop : {α : Type u_1} → OrderTop (Set α)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_inter_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₂.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The carrier set is closed under scalar multiplication.  -/
SubAddAction.vadd_mem' : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] (self : SubAddAction R M) (c : R) {x : M},
  x ∈ self.carrier → c +ᵥ x ∈ self.carrier
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instSubtypeMemValuationSubringValuationSubringAtPrime : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsDedekindDomain ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.map.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] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ φ_1 : W.RightFraction X Y),
  φ = φ_1 → ∀ (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L), φ.map L hL = φ_1.map L hL
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.density_ae_eq_limitProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s →
        (fun x => κ.density ν a x s) =ᵐ[ν a]
          MeasureTheory.Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s)
            (ProbabilityTheory.countableFiltration γ) (ν a)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkFunctor_obj_left : ∀ {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] (F : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G)
  (c : C), (CategoryTheory.Join.mkFunctor F G α).obj (CategoryTheory.Join.left c) = F.obj c
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_lt_self_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] (a : α) {b : α}, a - b < a ↔ 0 < b
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.triangle : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {f₁ f₂ f₃ : α → E}
  {g : α → F} {l : Filter α}, (f₁ - f₂) =O[𝕜; l] g → (f₂ - f₃) =O[𝕜; l] g → (f₁ - f₃) =O[𝕜; l] g
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorInl.eq_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  T.tensorInl =
    CategoryTheory.Limits.pushout.inl
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv
        (AlgebraicGeometry.Scheme.Hom.residueFieldMap f T.x))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv
        (AlgebraicGeometry.Scheme.Hom.residueFieldMap g T.y))
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_compl₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₂' : Type u_9} {n : Type u_11} {m : Type u_12} {m' : Type u_14}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m] [inst_8 : DecidableEq n]
  (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) [inst_9 : AddCommMonoid M₂'] [inst_10 : Module R M₂']
  (b₂' : Module.Basis m' R M₂') [inst_11 : Fintype m'] [inst_12 : DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R)
  (f : M₂' →ₗ[R] M₂),
  (LinearMap.toMatrix₂ b₁ b₂') (B.compl₂ f) = (LinearMap.toMatrix₂ b₁ b₂) B * (LinearMap.toMatrix b₂' b₂) f
-- Mathlib.Data.Finsupp.Order
Finsupp.mapDomain_nonpos : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  {f : ι → κ} {g : ι →₀ α}, g ≤ 0 → Finsupp.mapDomain f g ≤ 0
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) [inst_3 : F.Monoidal] (X : C) (X_1 : D),
  ((CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso
                  F).inv.app
            X).unmop.app
      X_1 =
    CategoryTheory.CategoryStruct.id ((F.obj X).unmop.obj X_1)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_biUnion_finset₀ : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Finset β} {t : β → Set α},
  (↑s).Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) t) →
    (∀ b ∈ s, MeasureTheory.NullMeasurableSet (t b) μ) →
      ∀ (f : α → ENNReal), ∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.differentiableAt_one_add_smoothingFn : ∀ {x : ℝ}, 1 < x → DifferentiableAt ℝ (fun z => 1 + AkraBazziRecurrence.smoothingFn z) x
-- Mathlib.Topology.Algebra.Group.Torsor
IsTopologicalAddTorsor.toContinuousVAdd : ∀ {V : Type u_1} {inst : AddGroup V} {inst_1 : TopologicalSpace V} {P : Type u_2} {inst_2 : AddTorsor V P}
  {inst_3 : TopologicalSpace P} [self : IsTopologicalAddTorsor P], ContinuousVAdd V P
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.addFn : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr
-- Mathlib.Data.Fintype.Card
Fintype.card_empty : Fintype.card Empty = 0
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- For `A B` two finite sets whose product has cardinality at least 2,
we can find at least two unique pairs.  -/
TwoUniqueSums.uniqueAdd_of_one_lt_card : ∀ {G : Type u_1} {inst : Add G} [self : TwoUniqueSums G] {A B : Finset G},
  1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueAdd A B p1.1 p1.2 ∧ UniqueAdd A B p2.1 p2.2
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
/-- See also `Matrix.coeff_charpolyRev_eq_neg_trace`.  -/
Matrix.trace_eq_neg_charpoly_coeff : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] [Nonempty n]
  (M : Matrix n n R), M.trace = -M.charpoly.coeff (Fintype.card n - 1)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_map : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → δ a},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.map f m)
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.IsNilpotent.dividedPowers.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] (hp : IsNilpotent ↑p) {I : Ideal A}
  [inst_2 : DecidablePred fun x => x ∈ I] (hIp : I ^ p = 0),
  DividedPowers.IsNilpotent.dividedPowers hp hIp = DividedPowers.OfInvertibleFactorial.dividedPowers ⋯ hIp
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquiv_mk : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] (I : Ideal R) (J : Ideal S) [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (x : R),
  (I.quotientEquiv J f hIJ) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) (f x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)},
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
    (∀ a ∈ t, (List.map Prod.fst l).contains a = false) →
      (Std.ExtDTreeMap.Const.insertMany t l).size = t.size + l.length
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.isFiniteMeasure : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν → ∀ᵐ (ω' : Ω') ∂ν, MeasureTheory.IsFiniteMeasure (κ ω')
-- Init.Internal.Order.MonadTail
Lean.Order.ST.bot' : {α σ : Type} →
  [inst : Nonempty α] → (s : Void σ) → Lean.Order.FlatOrder { val := Classical.ofNonempty, state := Classical.choice ⋯ }
-- Mathlib.Order.RelIso.Set
/-- `Set.inclusion` as a relation embedding.  -/
Subrel.inclusionEmbedding : {α : Type u_1} → (r : α → α → Prop) → {s t : Set α} → s ⊆ t → (Subrel r fun x => x ∈ s) ↪r Subrel r fun x => x ∈ t
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_le : ∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1]
  {m n : ℤ}, ↑m ≤ ↑n ↔ m ≤ n
-- Lean.Meta.SameCtorUtils
/-- Given a constructor, returns a mask of its fields, where `true` means that this field
occurs in the result type of the constructor.
 -/
Lean.Meta.occursInCtorTypeMask : Lean.Name → Lean.MetaM (Array Bool)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id X)]
  {Z : CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over X)}
  (h :
    (CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id X)).comp
        (CategoryTheory.Functor.id (CategoryTheory.Over X)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).unit
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id X)).whiskerLeft
          (CategoryTheory.ChosenPullbacksAlong.pullbackId X).hom)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).unit h
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `e` is `True`, `False`, or a literal value.
See `Lean.Meta.LitValues` for supported literals.
 -/
Lean.Meta.Grind.isInterpreted : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.Complex.Angle
Complex.angle_mul_right : ∀ {a : ℂ}, a ≠ 0 → ∀ (x y : ℂ), InnerProductGeometry.angle (x * a) (y * a) = InnerProductGeometry.angle x y
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Evaluation of functions into an indexed collection of semigroups at a point is a semigroup
homomorphism.
This is `Function.eval i` as a `MulHom`.  -/
Pi.evalMulHom : {I : Type u} → (f : I → Type v) → [inst : (i : I) → Mul (f i)] → (i : I) → ((i : I) → f i) →ₙ* f i
-- Mathlib.Data.PFunctor.Multivariate.W
/-- W-type of `P`  -/
MvPFunctor.W : {n : ℕ} → MvPFunctor.{u} (n + 1) → TypeVec.{u} n → Type u
-- Mathlib.Analysis.Normed.Order.Hom.Basic
GroupNormClass.toNormedCommGroup_norm_eq : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : CommGroup α] [inst_2 : GroupNormClass F α ℝ] (f : F)
  (x : α), ‖x‖ = f x
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ),
  ↑(Topology.RelCWComplex.skeleton C ↑n) ∪ ⋃ j, Topology.RelCWComplex.closedCell (n + 1) j =
    ↑(Topology.RelCWComplex.skeleton C (↑n + 1))
-- Mathlib.RingTheory.RingHom.Locally
/-- `Locally P` is local on the target.  -/
RingHom.locally_ofLocalizationSpanTarget : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] =>
      RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Lean.Elab.PreDefinition.Structural.FindRecArg
/-- Try each candidate argument combination for structural recursion.
Uses `commitIfNoEx` to backtrack on failure.
 -/
Lean.Elab.Structural.tryCandidates : {α : Type} →
  Array Lean.Name →
    Array Lean.Expr →
      Array Lean.Expr →
        Lean.Elab.Structural.RecArgCandidates → (Array Lean.Elab.Structural.RecArgInfo → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr.functor_obj_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  (X : CategoryTheory.Sheaf J A) {X_1 Y : Dᵒᵖ} (f : X_1 ⟶ Y),
  ((CategoryTheory.Equivalence.sheafCongr.functor J K e A).obj X).obj.map f = X.obj.map (e.inverse.map f.unop).op
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- Disjoint unions of locally path-connected spaces are locally path-connected.  -/
Sigma.locallyPathConnectedSpace : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), LocallyPathConnectedSpace (X i)], LocallyPathConnectedSpace ((i : ι) × X i)
-- Init.Data.SInt.Lemmas
instCommutativeInt8HMul : Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- A sphere centred at the origin in a valued ring is clopen.  -/
Valued.isClopen_sphere : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  {r : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀}, r ≠ 0 → IsClopen {x | Valued.v.restrict x = r}
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_symm_comp_map_rid_symm : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid M']
  [inst_6 : Module R M'] (f : M →ₗ[R] M'),
  ↑(TensorProduct.assoc R M' N R).symm ∘ₗ TensorProduct.map f ↑(TensorProduct.rid R N).symm =
    TensorProduct.map (TensorProduct.map f LinearMap.id) LinearMap.id ∘ₗ
      ↑(TensorProduct.rid R (TensorProduct R M N)).symm
-- Mathlib.Analysis.Calculus.FDeriv.Comp
DifferentiableAt.fun_comp' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (x : E) {f : E → F} {g : F → G},
  DifferentiableAt 𝕜 g (f x) → DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun x => g (f x)) x
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.instPreorder : {α : Type u_1} → [Preorder α] → Preorder (Topology.WithLowerSet α)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_range_succ_comm : ∀ {M : Type u_4} [inst : CommMonoid M] (f : ℕ → M) (n : ℕ),
  ∏ x ∈ Finset.range (n + 1), f x = f n * ∏ x ∈ Finset.range n, f x
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.associated_primPart_mul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p q : Polynomial R},
  p * q ≠ 0 → Associated (p * q).primPart (p.primPart * q.primPart)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.comp_aeval : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁) {B : Type u_2} [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (φ : S₁ →ₐ[R] B),
  φ.comp (MvPolynomial.aeval f) = MvPolynomial.aeval fun i => φ (f i)
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticOnNhd.zpow`

---

ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
AnalyticOnNhd.fun_zpow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E} {n : ℤ}, AnalyticOnNhd 𝕜 f s → (∀ z ∈ s, f z ≠ 0) → AnalyticOnNhd 𝕜 (fun i => f i ^ n) s
-- Init.Data.SInt.Lemmas
Int32.toISize_div_of_ne_left : ∀ (a b : Int32), a ≠ Int32.minValue → (a / b).toISize = a.toISize / b.toISize
-- Mathlib.LinearAlgebra.Matrix.Block
/-- An upper-left subblock of an invertible block-triangular matrix is invertible.  -/
Matrix.BlockTriangular.invertibleToBlock : {α : Type u_1} →
  {m : Type u_3} →
    {R : Type v} →
      {M : Matrix m m R} →
        {b : m → α} →
          [inst : CommRing R] →
            [inst_1 : DecidableEq m] →
              [inst_2 : Fintype m] →
                [inst_3 : LinearOrder α] →
                  [Invertible M] →
                    M.BlockTriangular b → (k : α) → Invertible (M.toBlock (fun i => b i < k) fun i => b i < k)
-- Mathlib.RepresentationTheory.Coinduced
Representation.coindMap_coe_apply : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  {A : Type u_4} {B : Type u_5} [inst_3 : AddCommMonoid A] [inst_4 : Module k A] [inst_5 : AddCommMonoid B]
  [inst_6 : Module k B] (σ : Representation k G A) (ρ : Representation k G B) (f : σ.IntertwiningMap ρ)
  (x : ↥(Representation.coindV φ σ)), ↑((Representation.coindMap φ f) x) = (f.compLeft H) ↑x
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.linear_inv_isBigO_right_add : ∀ (c e : ℤ) (z : ℂ), (fun d => (↑c * z + ↑d + ↑e)⁻¹) =O[Filter.cofinite] fun n => (↑n)⁻¹
-- Mathlib.Order.Partition.Basic
/-- When `α` is a frame, the meet `P ⊓ Q` of two partitions is the partition consisting of all
non-bottom meets `p ⊓ q` for `p ∈ P` and `q ∈ Q`.

Note that while finite meets of partitions can be constructed in this way, arbitrary meets generally
do not exist: for example when `α` is the frame of open subsets of the Cantor space, `Partition α`
has no bottom element.  -/
Partition.instSemilatticeInf : {α : Type u_2} → [inst : Order.Frame α] → (s : α) → SemilatticeInf (Partition s)
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.abs_inner_vsub_altitudeFoot_div_lt_one : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) [inst_4 : n.AtLeastTwo] {i j : Fin (n + 1)},
  i ≠ j → |inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j) / (s.height i * s.height j)| < 1
-- Mathlib.Data.ZMod.Basic
nsmul_zmod_val_inv_nsmul : ∀ {α : Type u_1} [inst : AddGroup α] {n : ℕ}, (Nat.card α).gcd n = 1 → ∀ (a : α), n • (↑n)⁻¹.val • a = a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_eq_default : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {a : α}, a ∉ m → m[a]! = default
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfo.mk.sizeOf_spec : ∀ (returnCont : Lean.Elab.Do.ReturnCont) (breakCont continueCont : Option (Lean.Elab.Do.DoElabM Lean.Expr)),
  sizeOf { returnCont := returnCont, breakCont := breakCont, continueCont := continueCont } =
    1 + sizeOf returnCont + sizeOf breakCont + sizeOf continueCont
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} {α β : F ⟶ G} (h : α = β)
  (X : CategoryTheory.Endofunctor.Coalgebra F),
  ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq h).hom.app X).f = CategoryTheory.CategoryStruct.id X.V
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coeToPowerSeries.ringHom_apply : ∀ {R : Type u_1} [inst : Semiring R] {φ : Polynomial R}, Polynomial.coeToPowerSeries.ringHom φ = ↑φ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipSuffixWhile_eq_endPos_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String.Slice},
  s.skipSuffixWhile pat = s.endPos ↔ s.endsWith pat = false
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.comp_concaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α},
  StrictConvexOn 𝕜 (f '' s) g → ConcaveOn 𝕜 s f → AntitoneOn g (f '' s) → Set.InjOn f s → StrictConvexOn 𝕜 s (g ∘ f)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof → Sort u}
  (t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_2 t (Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.brecOn.go t F_1 F_2).2
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.le_iff : ∀ {X : SSet} {A : X.Subcomplex} {x y : A.N}, x ≤ y ↔ x.toN ≤ y.toN