mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.topologicalSpace.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) [inst : (i : ι) → TopologicalSpace (R i)],
  RestrictedProduct.topologicalSpace R A 𝓕 =
    ⨆ S,
      ⨆ (hS : 𝓕 ≤ Filter.principal S),
        TopologicalSpace.coinduced (RestrictedProduct.inclusion R A hS)
          (TopologicalSpace.induced DFunLike.coe inferInstance)
-- Mathlib.Algebra.Field.Defs
/-- Scalar multiplication by a rational number.

Unless there is a risk of a `Module ℚ _` instance diamond, write `qsmul := _`. This will set
`qsmul` to `(Rat.cast · * ·)` thanks to unification in the default proof of `qsmul_def`.

Do not use directly. Instead use the `•` notation.  -/
DivisionRing.qsmul : {K : Type u_2} → [self : DivisionRing K] → ℚ → K → K
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_neg_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddRightStrictMono α] (a : α) {b : α}, b < 0 → b + a < a
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- Reindex a categorical biproduct via an equivalence of the index types.  -/
CategoryTheory.Limits.biproduct.reindex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {β γ : Type} →
        [Finite β] →
          (ε : β ≃ γ) →
            (f : γ → C) →
              [inst_3 : CategoryTheory.Limits.HasBiproduct f] →
                [inst_4 : CategoryTheory.Limits.HasBiproduct (f ∘ ⇑ε)] → ⨁ f ∘ ⇑ε ≅ ⨁ f
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_inverse_map_app_app : ∀ {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] {X Y : CategoryTheory.Functor (C × D) E} (T : X ⟶ Y)
  (X_1 : C) (Y_1 : D), ((CategoryTheory.Functor.currying.inverse.map T).app X_1).app Y_1 = T.app (X_1, Y_1)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (r : ↑(X.presheaf.obj (Opposite.op ⊤))),
      AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map (X.basicOpen r).ι.base).obj U)
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.instHasInvolutiveReverseSymmetrify : {V : Type u_2} → [inst : Quiver V] → Quiver.HasInvolutiveReverse (Quiver.Symmetrify V)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHom_apply : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : (i : ι) → AddCommGroup (A i)] (n : ℕ) (x : (i : ι) → A i),
  (QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHom A n) ↑x = fun i => ↑(x i)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.mem_Lp_of_ae_bound : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] {f : α →ₘ[μ] E} (C : ℝ),
  (∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ C) → f ∈ MeasureTheory.Lp E p μ
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions on domains is `C^n`.  -/
ContDiffOn.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : F → G}
  {f : E → F}, ContDiffOn 𝕜 n g t → ContDiffOn 𝕜 n f s → Set.MapsTo f s t → ContDiffOn 𝕜 n (g ∘ f) s
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.SameCycle.mem_support_iff : ∀ {α : Type u_2} {x y : α} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α],
  f.SameCycle x y → (x ∈ f.support ↔ y ∈ f.support)
-- Mathlib.Data.Prod.Lex
Prod.Lex.toLex_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β], StrictMono ⇑toLex
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  {f g : A ⟶ B}, f = g ↔ f.val = g.val
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The natural isomorphism witnessing the pseudo-unity constraint of `CoGrothendieck.map`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.mapIdIso : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) →
      CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.id F) ≅
        CategoryTheory.Functor.id F.CoGrothendieck
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.coweightMap_one : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  RootPairing.Hom.coweightMap 1 = LinearMap.id
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h =
    (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' (CategoryTheory.ShortComplex.opMap φ) h.op).unop
-- Mathlib.Order.Minimal
MinimalFor.maximal_of_strictAntiOn : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {g : α → β},
  StrictAntiOn g (Set.ofPred P) → MinimalFor P g x → Maximal P x
-- Lean.Meta.Tactic.Grind.Internalize
Lean.Meta.Grind.activateTheorem : Lean.Meta.Grind.EMatchTheorem → ℕ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
/-- Bundled `n` times continuously differentiable sections of a vector bundle.
Denoted as `Cₛ^n⟮I; F, V⟯` within the `Manifold` namespace.  -/
Manifold.«termCₛ^_⟮_;_,_⟯» : Lean.ParserDescr
-- Mathlib.RingTheory.Kaehler.Polynomial
KaehlerDifferential.mvPolynomialBasis_repr_comp_D : ∀ (R : Type u) [inst : CommRing R] (σ : Type u_1),
  (↑(KaehlerDifferential.mvPolynomialBasis R σ).repr).compDer (KaehlerDifferential.D R (MvPolynomial σ R)) =
    MvPolynomial.mkDerivation R fun x => fun₀ | x => 1
-- Mathlib.Algebra.Module.Presentation.Tensor
Module.Presentation.tensor_relation : ∀ {A : Type u} [inst : CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module A M₁] [inst_4 : Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂)
  (x : pres₁.R × pres₂.G ⊕ pres₁.G × pres₂.R),
  (pres₁.tensor pres₂).relation x =
    match x with
    | Sum.inl (r₁, g₂) => Finsupp.embDomain (Function.Embedding.sectL pres₁.G g₂) (pres₁.relation r₁)
    | Sum.inr (g₁, r₂) => Finsupp.embDomain (Function.Embedding.sectR g₁ pres₂.G) (pres₂.relation r₂)
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIoo_filter : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G],
  (SummationFilter.symmetricIoo G).filter = Filter.map (fun g => Finset.Ioo (-g) g) Filter.atTop
-- Mathlib.CategoryTheory.Category.Cat
/-- Embedding `Type` into `Cat` as discrete categories.

This ought to be modelled as a 2-functor!
 -/
CategoryTheory.typeToCat : CategoryTheory.Functor (Type u) CategoryTheory.Cat
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_zero : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : Zero α], ↑0 = 0
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {X : C} {grp : CategoryTheory.GrpObj X}
  {comm : CategoryTheory.IsCommMonObj X} {X_1 : C} {grp_1 : CategoryTheory.GrpObj X_1}
  {comm_1 : CategoryTheory.IsCommMonObj X_1},
  { X := X, grp := grp, comm := comm } = { X := X_1, grp := grp_1, comm := comm_1 } → X = X_1 ∧ grp ≍ grp_1
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.ι_comp_isoPointwiseLeftKanExtension_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (F G : CategoryTheory.MonoidalCategory.DayFunctor C V) (x y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        ((CategoryTheory.CostructuredArrow.proj (CategoryTheory.MonoidalCategory.tensor C)
              (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)).comp
          (CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor))
        (CategoryTheory.CostructuredArrow.mk
          (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj x y))))
      ((F.isoPointwiseLeftKanExtension G).inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
    (F.η G).app (x, y)
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.defEvalConfigItem.checkStruct : Lean.Ident → Lean.Name → Lean.MetaM Unit
-- Mathlib.Analysis.Calculus.FDeriv.Affine
ContinuousAffineMap.differentiableAt : ∀ {𝕜 : 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] (f : E →ᴬ[𝕜] F)
  {x : E}, DifferentiableAt 𝕜 (⇑f) x
-- Mathlib.Topology.Homotopy.LocallyContractible
/-- In a strongly locally contractible space, for any open set `U` containing `x`, there is a basis
of contractible neighborhoods of `x` contained in `U`.  -/
contractible_subset_basis : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} [StronglyLocallyContractibleSpace X] {U : Set X},
  IsOpen U → x ∈ U → (nhds x).HasBasis (fun s => s ∈ nhds x ∧ ContractibleSpace ↑s ∧ s ⊆ U) id
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union m₂ ⋯ ⋯).get? k = m₂.get? k
-- Lean.Elab.Match
Lean.Elab.Term.PatternElabException.mk.inj : ∀ {ex : Lean.Exception} {patternIdx : ℕ} {pathToIndex : List ℕ} {ex_1 : Lean.Exception} {patternIdx_1 : ℕ}
  {pathToIndex_1 : List ℕ},
  { ex := ex, patternIdx := patternIdx, pathToIndex := pathToIndex } =
      { ex := ex_1, patternIdx := patternIdx_1, pathToIndex := pathToIndex_1 } →
    ex = ex_1 ∧ patternIdx = patternIdx_1 ∧ pathToIndex = pathToIndex_1
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- In an `n`-preprimitive action, the action of `fixingAddSubgroup M s`
on `ofFixingAddSubgroup M s` is preprimitive, for all sets `s` such that `s.encard + 1 = n`.  -/
AddAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup : ∀ (M : Type u_1) {α : Type u_2} {inst : AddGroup M} {inst_1 : AddAction M α} (n : ℕ)
  [self : AddAction.IsMultiplyPreprimitive M α n] {s : Set α},
  s.encard + 1 = ↑n → AddAction.IsPreprimitive ↥(fixingAddSubgroup M s) ↥(SubAddAction.ofFixingAddSubgroup M s)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.comp_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''} {u : Set M'} {y : M'},
  MDiffAt[u] g y → MDiffAt[s] f x → s ⊆ f ⁻¹' u → f x = y → MDiffAt[s] (g ∘ f) x
-- Mathlib.Data.Finset.NoncommProd
Finset.mul_noncommProd_erase : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : DecidableEq α] (s : Finset α) {a : α},
  a ∈ s →
    ∀ (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f))
      (comm' : optParam (∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → Function.onFun Commute f x x_1) ⋯),
      f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.congr_left : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ m₃ : Std.DHashMap.Raw α β}, m₁.Equiv m₂ → (m₁.Equiv m₃ ↔ m₂.Equiv m₃)
-- Mathlib.Data.Vector.Basic
List.Vector.ne_cons_iff : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n.succ) (v' : List.Vector α n),
  v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'
-- Mathlib.RingTheory.RingInvo
RingInvo.mk : {R : Type u_2} →
  [inst : Semiring R] →
    (toRingEquiv : R ≃+* Rᵐᵒᵖ) →
      (∀ (x : R), MulOpposite.unop (toRingEquiv.toFun (MulOpposite.unop (toRingEquiv.toFun x))) = x) → RingInvo R
-- Mathlib.Data.List.Sigma
/-- Remove the first pair with the key `a`.  -/
List.kerase : {α : Type u} → {β : α → Type v} → [DecidableEq α] → α → List (Sigma β) → List (Sigma β)
-- Mathlib.Order.Booleanisation
Booleanisation.LE.lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α},
  a ≤ b → (Booleanisation.lift a).LE (Booleanisation.lift b)
-- Mathlib.RingTheory.Algebraic.Basic
isAlgebraic_natCast : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R] (n : ℕ),
  IsAlgebraic R ↑n
-- Mathlib.Data.Multiset.DershowitzManna
/-- `IsDershowitzMannaLT` is transitive.  -/
Multiset.IsDershowitzMannaLT.trans : ∀ {α : Type u_1} [inst : Preorder α] {M N P : Multiset α},
  M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instIsSubApplyForall : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂], IsSubApply (MultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.var : Nat.Internal.Linear.Var → Nat.Internal.SOM.Expr
-- Std.Time.Zoned.TimeZone
/-- Creates a `Timestamp` from a given number of hour.
 -/
Std.Time.TimeZone.ofHours : String → String → Std.Time.Hour.Offset → optParam Bool false → Std.Time.TimeZone
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseRightKanExtension F L]
  [inst_5 : L.HasPointwiseRightKanExtension F] (a : A),
  CategoryTheory.CategoryStruct.comp ((G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a))
      ((L.pointwiseRightKanExtensionCounit (F.comp G)).app a) =
    G.map ((L.pointwiseRightKanExtensionCounit F).app a)
-- Init.Data.Order.FactoriesExtra
Std.isLE_compare : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α] {a b : α}, (compare a b).isLE = true ↔ a ≤ b
-- Mathlib.Computability.TuringMachine.Config
/-- The type of codes for primitive recursive functions. Unlike `Nat.Partrec.Code`, this uses a set
of operations on `List ℕ`. See `Code.eval` for a description of the behavior of the primitives.  -/
Turing.ToPartrec.Code : Type
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality**: The geometric mean is less than or equal to the arithmetic mean, weighted
version for real-valued nonnegative functions.  -/
Real.geom_mean_le_arith_mean_weighted : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) → ∑ i ∈ s, w i = 1 → (∀ i ∈ s, 0 ≤ z i) → ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- Cardinality of a Young diagram  -/
YoungDiagram.card : YoungDiagram → ℕ
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.differentiableWithinAt : ∀ {𝕜 : 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} (iso : E ≃ₗᵢ[𝕜] F), DifferentiableWithinAt 𝕜 (⇑iso) s x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₂ → (t₁ \ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwLemma.mk.injEq : ∀ (name : Mathlib.Tactic.ClickSuggestions.Premise) (symm : Bool) (name_1 : Mathlib.Tactic.ClickSuggestions.Premise)
  (symm_1 : Bool),
  ({ name := name, symm := symm } = { name := name_1, symm := symm_1 }) = (name = name_1 ∧ symm = symm_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_sub_natCast' : ∀ {y : ℝ} {n : ℕ}, y - ↑n ≠ 0 → ∀ (x : NNReal), x ^ (y - ↑n) = x ^ y / x ^ n
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.distinguished' : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (self : CategoryTheory.Triangulated.SpectralObject C ι) (D : CategoryTheory.ComposableArrows ι 2),
  CategoryTheory.Pretriangulated.Triangle.mk
      (self.ω₁.map
        ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
              CategoryTheory.Triangulated.SpectralObject._proof_6 CategoryTheory.Triangulated.SpectralObject._proof_8
              CategoryTheory.Triangulated.SpectralObject._proof_10 CategoryTheory.Triangulated.SpectralObject._proof_2
              CategoryTheory.Triangulated.SpectralObject._proof_4).app
          D))
      (self.ω₁.map
        ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
              CategoryTheory.Triangulated.SpectralObject._proof_8 CategoryTheory.Triangulated.SpectralObject._proof_2
              CategoryTheory.Triangulated.SpectralObject._proof_6 CategoryTheory.Triangulated.SpectralObject._proof_4
              CategoryTheory.Triangulated.SpectralObject._proof_4).app
          D))
      (self.δ'.app D) ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Algebra.Module.Torsion.Basic
/-- An `(R ⧸ I)`-module is an `R`-module which `IsTorsionBySet R M I`.  -/
Module.IsTorsionBySet.module : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {I : Ideal R} → [inst_3 : I.IsTwoSided] → Module.IsTorsionBySet R M ↑I → Module (R ⧸ I) M
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_pos_iff : ∀ {x : ℝ}, 0 ≤ x → (0 < Real.log x ↔ 1 < x)
-- Init.WF
/-- Attaches to `x` the proof that `x` is accessible in the given well-founded relation.
This can be used in recursive function definitions to explicitly use a different relation
than the one inferred by default:

```
def otherWF : WellFounded Nat := …
def foo (n : Nat) := …
termination_by otherWF.wrap n
```
 -/
WellFounded.wrap : {α : Sort u} → {r : α → α → Prop} → WellFounded r → α → { x // Acc r x }
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Construct a morphism between categorical products from a family of morphisms between the
factors.  -/
CategoryTheory.Limits.Pi.map' : {β : Type w} →
  {α : Type w₂} →
    {C : Type u} →
      [inst : CategoryTheory.Category.{v, u} C] →
        {f : α → C} →
          {g : β → C} →
            [inst_1 : CategoryTheory.Limits.HasProduct f] →
              [inst_2 : CategoryTheory.Limits.HasProduct g] → (p : β → α) → ((b : β) → f (p b) ⟶ g b) → (∏ᶜ f ⟶ ∏ᶜ g)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.sle_eq_ult : ∀ {w : ℕ} (x y : BitVec w), x.sle y = !(!x.getLsbD (w - 1) == y.getLsbD (w - 1) ^^ y.ult x)
-- Init.Data.String.Termination
String.Pos.instWellFoundedRelation : {s : String} → WellFoundedRelation s.Pos
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftId_hom_app_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.mapLeftId L R).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Lean.Syntax
_private.Lean.Syntax.0.Lean.Syntax.reprint.reprintLeaf : Lean.SourceInfo → String → String
-- Mathlib.Data.List.Zip
List.zipWith3_same_left : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → α → β → γ) (la : List α) (lb : List β),
  List.zipWith3 f la la lb = List.zipWith (fun a b => f a a b) la lb