mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1), (AffineMap.lineMap p₀ p₁).linear = LinearMap.id.smulRight (p₁ -ᵥ p₀)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.target_eq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B} (self : Bundle.Trivialization F proj),
  self.target = self.baseSet ×ˢ Set.univ
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- A based category over `𝒮` is a category `𝒳` together with a functor `p : 𝒳 ⥤ 𝒮`.  -/
CategoryTheory.BasedCategory : (𝒮 : Type u₁) → [CategoryTheory.Category.{v₁, u₁} 𝒮] → Type (max (max (max u₁ (u₂ + 1)) v₁) (v₂ + 1))
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.dropInfix?.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (List α) → Sort u_2) (s : List α) (h_1 : Unit → motive none)
  (h_2 : (s : List α) → motive (some s)),
  (match some s with
    | none => h_1 ()
    | some s => h_2 s) =
    h_2 s
-- Mathlib.Tactic.NormNum.Eq
_private.Mathlib.Tactic.NormNum.Eq.0.Mathlib.Meta.NormNum.evalEq.intArm : {v : Lean.Level} →
  {β : Q(Type v)} →
    (e : Q(«$β»)) →
      (u : Lean.Level) →
        (α :
            have u := u;
            Q(Type u)) →
          (a b : Q(«$α»)) →
            Mathlib.Meta.NormNum.Result a →
              Mathlib.Meta.NormNum.Result b → Q(Ring «$α») → Lean.MetaM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.RingTheory.Finiteness.FiniteTypeLocal
/-- Let `S` be an `R`-algebra, `M` a submonoid of `R`, and `S' = M⁻¹S`.
If the image of some `x : S` falls in the adjoin of some finite `s ⊆ S'` over `R`,
then there exists some `m : M` such that `m • x` falls in the
adjoin of `IsLocalization.finsetIntegerMultiple _ s` over `R`.
 -/
IsLocalization.lift_mem_adjoin_finsetIntegerMultiple : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R)
  {S' : Type u_4} [inst_3 : CommRing S'] [inst_4 : Algebra S S'] [inst_5 : Algebra R S'] [IsScalarTower R S S']
  [inst_7 : IsLocalization (Submonoid.map (algebraMap R S) M) S'] (x : S) (s : Finset S'),
  (algebraMap S S') x ∈ Algebra.adjoin R ↑s →
    ∃ m, m • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.not_ite_beq' : ∀ {a b c : Bool}, ((!bif c then b else a) == a) = (c && a == !b)
-- Mathlib.LinearAlgebra.TensorProduct.Associator
/-- This special case is worth defining explicitly since it is useful for defining multiplication
on tensor products of modules carrying multiplications (e.g., associative rings, Lie rings, ...).

E.g., suppose `M = P` and `N = Q` and that `M` and `N` carry bilinear multiplications:
`M ⊗ M → M` and `N ⊗ N → N`. Using `map`, we can define `(M ⊗ M) ⊗ (N ⊗ N) → M ⊗ N` which, when
combined with this definition, yields a bilinear multiplication on `M ⊗ N`:
`(M ⊗ N) ⊗ (M ⊗ N) → M ⊗ N`. In particular we could use this to define the multiplication in
the `TensorProduct.semiring` instance (currently defined "by hand" using `TensorProduct.mul`).

See also `mul_mul_mul_comm`.  -/
TensorProduct.tensorTensorTensorComm : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_5) →
      (N : Type u_6) →
        (P : Type u_7) →
          (Q : Type u_8) →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid N] →
                [inst_3 : AddCommMonoid P] →
                  [inst_4 : AddCommMonoid Q] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R N] →
                        [inst_7 : Module R Q] →
                          [inst_8 : Module R P] →
                            TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) ≃ₗ[R]
                              TensorProduct R (TensorProduct R M P) (TensorProduct R N Q)
-- Lean.Elab.Deriving.Basic
/-- Registers a deriving handler for a class. This function should be called in an `initialize` block.

A `DerivingHandler` is called on the fully qualified names of all types it is running for. For
example, `deriving instance Foo for Bar, Baz` invokes ``fooHandler #[`Bar, `Baz]``.
 -/
Lean.Elab.registerDerivingHandler : Lean.Name → Lean.Elab.DerivingHandler → IO Unit
-- Mathlib.Topology.LocallyConstant.Basic
/-- Given a clopen set `U` and a locally constant function `f`, `LocallyConstant.mulIndicator`
returns the locally constant function that is `f` on `U` and `1` otherwise.  -/
LocallyConstant.mulIndicator : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {R : Type u_5} → [One R] → {U : Set X} → LocallyConstant X R → IsClopen U → LocallyConstant X R
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.restrictMonoidHom.eq_1 : ∀ {𝕜 : 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 : Monoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffMul I' n G] {U V : TopologicalSpace.Opens N} (h : U ≤ V),
  ContMDiffMap.restrictMonoidHom I I' G h =
    { toFun := fun f => ⟨⇑f ∘ Set.inclusion h, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_comap_eq_self : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N} {S : Subsemigroup N},
  S ≤ f.srange → Subsemigroup.map f (Subsemigroup.comap f S) = S
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_fun_sum : ∀ {𝕜 : 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] {x : E}
  {s : Set E} {ι : Type u_4} {u : Finset ι} {A : ι → E → F},
  UniqueDiffWithinAt 𝕜 s x →
    (∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) →
      fderivWithin 𝕜 (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, fderivWithin 𝕜 (A i) s x
-- Init.Data.Fin.Lemmas
Fin.subsingleton_zero : Subsingleton (Fin 0)
-- Lean.Parser.Extra
Lean.Parser.antiquotNestedExpr.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Stream.Defs
/-- Nonempty initial segments of a stream.  -/
Stream'.inits : {α : Type u} → Stream' α → Stream' (List α)
-- Lean.CoreM
_private.Lean.CoreM.0.Lean.compileDeclsImpl : Array Lean.Name → Lean.CoreM Unit
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.whiskerRight_left_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R))
      (CategoryTheory.Limits.pullback.snd T.hom R.hom) =
    CategoryTheory.Limits.pullback.snd S.hom R.hom
-- Mathlib.Data.Finsupp.Basic
Finsupp.prod_filter_mul_prod_filter_not : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M)
  [inst_2 : CommMonoid N] (g : α → M → N),
  (Finsupp.filter p f).prod g * (Finsupp.filter (fun a => ¬p a) f).prod g = f.prod g
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The coarsening of a valuation ring associated to a prime ideal.  -/
ValuationSubring.ofPrime : {K : Type u} → [inst : Field K] → (A : ValuationSubring K) → (P : Ideal ↥A) → [P.IsPrime] → ValuationSubring K
-- Mathlib.RingTheory.Algebraic.Basic
/-- If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R,
and the map from `R` to `S` is injective.  -/
Algebra.IsAlgebraic.extendScalars : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A],
  Function.Injective ⇑(algebraMap R S) → ∀ [Algebra.IsAlgebraic R A], Algebra.IsAlgebraic S A
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A cokernel-preserving functor between preadditive categories preserves any pair being
a colimit.  -/
CategoryTheory.Functor.preservesCoproduct_of_preservesCokernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  {X Y : C}, CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) F
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.modify_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : β k → β k}, m.modify k f = ∅ ↔ m = ∅
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.sclosure_preimage_le : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S]
  [inst_2 : NonUnitalNonAssocSemiring S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (s : Set S),
  NonUnitalSubsemiring.closure (⇑f ⁻¹' s) ≤ NonUnitalSubsemiring.comap f (NonUnitalSubsemiring.closure s)
-- Mathlib.Algebra.Group.Defs
/-- An abbreviation for `nsmulBinRec` with an additional typeclass assumption on associativity
so that we can use it in `@[csimp]` for more performant code generation
as an automatic parameter.  -/
nsmulBinRecAuto : {M : Type u_2} → [AddSemigroup M] → [Zero M] → ℕ → M → M
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.one_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → One (R i)] [inst_2 : ∀ (i : ι), OneMemClass (S i) (R i)] (i : ι), 1 i = 1
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.generateSetAlgebra.below.union : ∀ {α : Type u_2} {𝒜 : Set (Set α)} {motive : (a : Set α) → MeasureTheory.generateSetAlgebra 𝒜 a → Prop} (s t : Set α)
  (hs : MeasureTheory.generateSetAlgebra 𝒜 s) (ht : MeasureTheory.generateSetAlgebra 𝒜 t),
  MeasureTheory.generateSetAlgebra.below hs →
    motive s hs → MeasureTheory.generateSetAlgebra.below ht → motive t ht → MeasureTheory.generateSetAlgebra.below ⋯
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_le_unop_iff : ∀ {M : Type u_2} [inst : Add M] {S₁ S₂ : AddSubsemigroup Mᵃᵒᵖ}, S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
-- Mathlib.Algebra.Polynomial.Module.AEval
LinearMap.ofAEval.eq_1 : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] {N : Type u_4} [inst_7 : AddCommMonoid N] [inst_8 : Module R N]
  [inst_9 : Module (Polynomial R) N] [inst_10 : IsScalarTower R (Polynomial R) N] (f : M →ₗ[R] N)
  (hf : ∀ (m : M), f (a • m) = Polynomial.X • f m),
  LinearMap.ofAEval a f hf = { toAddHom := (f ∘ₗ ↑(Module.AEval.of R M a).symm).toAddHom, map_smul' := ⋯ }
-- Mathlib.Analysis.Meromorphic.Order
meromorphicOrderAt.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (x : 𝕜),
  meromorphicOrderAt f x =
    if hf : MeromorphicAt f x then
      ENat.map (fun x => ↑x) (analyticOrderAt (fun z => (z - x) ^ Exists.choose hf • f z) x) - ↑(Exists.choose hf)
    else 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.edges_dropUntil_suffix_edges : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).edges <:+ p.edges
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.hasDimensionLT_subcomplex_top_iff : ∀ (X : SSet) (d : ℕ), ⊤.toSSet.HasDimensionLT d ↔ X.HasDimensionLT d
-- Mathlib.Topology.Separation.Basic
instR0SpaceForall : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R0Space (X i)],
  R0Space ((i : ι) → X i)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) (y : Bᵒᵖ),
  ((CategoryTheory.Bicategory.yoneda₀ x).obj y).str = CategoryTheory.Bicategory.homCategory (Opposite.unop y) x
-- Lean.Elab.Binders
Lean.Elab.Term.FunBinders.State.mk.inj : ∀ {fvars : Array Lean.Expr} {lctx : Lean.LocalContext} {localInsts : Lean.LocalInstances}
  {expectedType? : Option Lean.Expr} {fvars_1 : Array Lean.Expr} {lctx_1 : Lean.LocalContext}
  {localInsts_1 : Lean.LocalInstances} {expectedType?_1 : Option Lean.Expr},
  { fvars := fvars, lctx := lctx, localInsts := localInsts, expectedType? := expectedType? } =
      { fvars := fvars_1, lctx := lctx_1, localInsts := localInsts_1, expectedType? := expectedType?_1 } →
    fvars = fvars_1 ∧ lctx = lctx_1 ∧ localInsts = localInsts_1 ∧ expectedType? = expectedType?_1
-- Mathlib.CategoryTheory.Square
/-- The equivalence `Square C ≌ Arrow (Arrow C)` which sends a
commutative square `sq` to the obvious arrow from the top morphism of `sq`
to the bottom morphism of `sq`.  -/
CategoryTheory.Square.arrowArrowEquivalence' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C ≌ CategoryTheory.Arrow (CategoryTheory.Arrow C)
-- Init.Data.Vector.Lemmas
Vector.flatMap_mk : ∀ {α : Type u_1} {β : Type u_2} {m n : ℕ} {f : α → Vector β m} {xs : Array α} (h : xs.size = n),
  (Vector.mk xs h).flatMap f = Vector.mk (Array.flatMap (fun a => (f a).toArray) xs) ⋯
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
/-- The weight space of a root pairing.  -/
RootPairingCat.weight : {R : Type u} → [inst : CommRing R] → RootPairingCat R → Type v
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.restrictScalars_injective : ∀ (K : Type u_1) {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] [inst_5 : Algebra L' L] [inst_6 : IsScalarTower K L' L],
  Function.Injective (IntermediateField.restrictScalars K)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If `s` is a limit binary fan over `X` and `Y`, then every pair of morphisms `f : W ⟶ X` and
`g : W ⟶ Y` induces a morphism `l : W ⟶ s.pt` satisfying `l ≫ s.fst = f` and `l ≫ s.snd = g`.
 -/
CategoryTheory.Limits.BinaryFan.IsLimit.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y W : C} →
      {s : CategoryTheory.Limits.BinaryFan X Y} → CategoryTheory.Limits.IsLimit s → (W ⟶ X) → (W ⟶ Y) → (W ⟶ s.pt)
-- Std.Time.Format.Modifier
Std.Time.instInhabitedYear.default : Std.Time.Year
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_sSup : ∀ {G : Type u_2} [inst : AddGroup G] (S : Set (AddSubgroup Gᵃᵒᵖ)), (sSup S).unop = sSup (AddSubgroup.op ⁻¹' S)
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.pairSet_empty_eq_empty : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] [inst_1 : DecidableEq T] (a c : ENNReal), PairReduction.pairSet ∅ a c = ∅
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticMap.tmul.eq_1 : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [inst : CommRing R]
  [inst_1 : CommRing A] [inst_2 : AddCommGroup M₁] [inst_3 : AddCommGroup M₂] [inst_4 : AddCommGroup N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Algebra R A] [inst_7 : Module R M₁] [inst_8 : Module A M₁] [inst_9 : Module R N₁]
  [inst_10 : Module A N₁] [inst_11 : SMulCommClass R A M₁] [inst_12 : IsScalarTower R A M₁]
  [inst_13 : IsScalarTower R A N₁] [inst_14 : Module R M₂] [inst_15 : Module R N₂] [inst_16 : Invertible 2]
  (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂), Q₁.tmul Q₂ = (QuadraticMap.tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
          (CategoryTheory.CategoryStruct.id Z))
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y
            Z).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W)
        (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The constant 0 map is linear.  -/
LinearMap.instZero : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R₁ M] → [inst_5 : Module R₂ M₂] → {σ₁₂ : R₁ →+* R₂} → Zero (M →ₛₗ[σ₁₂] M₂)
-- Mathlib.CategoryTheory.Sites.Monoidal
CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} A]
  [inst_2 : CategoryTheory.MonoidalCategory A] [inst_3 : CategoryTheory.MonoidalClosed A] (M : A)
  (F G : CategoryTheory.Functor Cᵒᵖ A) [inst_4 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom A F G]
  (X : C),
  CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv M F G X =
    {
      toFun := fun f =>
        {
          app := fun j =>
            CategoryTheory.MonoidalClosed.uncurry
              (CategoryTheory.CategoryStruct.comp f
                (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ A
                  ((CategoryTheory.Under.forget (Opposite.op X)).comp F)
                  ((CategoryTheory.Under.forget (Opposite.op X)).comp G)
                  (CategoryTheory.Under.mk (Opposite.unop j).hom.op))),
          naturality := ⋯ },
      invFun := fun g =>
        CategoryTheory.Limits.end_.lift
          (fun j => CategoryTheory.MonoidalClosed.curry (g.app (Opposite.op (CategoryTheory.Over.mk j.hom.unop)))) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instDistribMulAction : {S : Type u_2} →
  {R : Type u_3} →
    {A : Type u_4} →
      [inst : Monoid S] →
        [inst_1 : AddMonoid R] →
          [inst_2 : AddMonoid A] →
            [DistribMulAction S R] → [DistribMulAction S A] → DistribMulAction S (Unitization R A)
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.hasCentralRadical_of_radical_le : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.radical R L ≤ LieAlgebra.center R L → LieAlgebra.HasCentralRadical R L
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_update : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R) (x : AddMonoidAlgebra R M),
  (AddMonoidAlgebra.update m r x).coeff = x.coeff.update m r
-- Mathlib.Data.Analysis.Topology
LocallyFinite.Realizer.mk : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      {F : Ctop.Realizer α} →
        {f : β → Set α} →
          (bas : (a : α) → { s // a ∈ F.F.f s }) →
            ((x : α) → Fintype ↑{i | (f i ∩ F.F.f ↑(bas x)).Nonempty}) → LocallyFinite.Realizer F f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.alter.match_3.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.gt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.gt = Ordering.gt → motive Ordering.gt) (h_3 : Ordering.gt = Ordering.eq → motive Ordering.eq),
  (match h : Ordering.gt with
    | Ordering.lt => h_1 h
    | Ordering.gt => h_2 h
    | Ordering.eq => h_3 h) =
    h_2 ⋯
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.coe_one : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ⇑1 = id
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isSome_getElem?_iff_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m[a]?.isSome = true ↔ a ∈ m
-- Mathlib.Algebra.Homology.Embedding.Extend
ComplexShape.Embedding.instFullHomologicalComplexExtendFunctor : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C], (e.extendFunctor C).Full
-- Lean.Meta.Tactic.Grind.EMatch
/-- Entry point for matching `lhs ←= rhs` patterns.
It traverses disequalities `a = b`, and tries to solve two matching problems:
1- match `lhs` with `a` and `rhs` with `b`
2- match `lhs` with `b` and `rhs` with `a`
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.matchEqBwdPat : Lean.Expr → Lean.Meta.Grind.EMatch.M Unit
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.addPrimeToFVarUserNames : Array Lean.Expr → Lean.LocalContext → Lean.LocalContext
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.neg_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] (f : CompactlySupportedContinuousMap α β), (-f) x = -f x
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_subset_smul_right : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s₁ s₂ : Finset α} {t : Finset β},
  s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff : ∀ {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₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D₁ : Type u_1} {D₂ : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D₁] [inst_3 : CategoryTheory.Category.{v_2, u_2} D₂]
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
  (F : CategoryTheory.Functor D₁ D₂) [Φ.HasRightResolutions] (e : Φ.functor.comp L₂ ≅ L₁.comp F),
  Φ.IsRightDerivabilityStructure ↔ CategoryTheory.TwoSquare.GuitartExact e.hom
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.instHasEqualizerFstPiMapSndPiMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I]
  [inst_2 : CategoryTheory.Limits.HasProduct I.left] [inst_3 : CategoryTheory.Limits.HasProduct I.right],
  CategoryTheory.Limits.HasEqualizer I.fstPiMap I.sndPiMap
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.find?_toArray_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {k : α} {v : β k}, m.WF → (Array.find? (fun x => x.fst == k) m.toArray = some ⟨k, v⟩ ↔ m.get? k = some v)