mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sat.AIG.Lemmas
/-- `AIG.mkGate` never shrinks the underlying AIG.
 -/
Std.Sat.AIG.mkGate_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.decls.size ≤ (aig.mkGate input).aig.decls.size
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_update_add : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι)
  (x y : M₁ i), f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)
-- Init.Data.BitVec.Bootstrap
BitVec.toNat_setWidth' : ∀ {m n : ℕ} (p : m ≤ n) (x : BitVec m), (BitVec.setWidth' p x).toNat = x.toNat
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.stx.injEq : ∀ (id : Lean.Name) (ref : Lean.Syntax) (id_1 : Lean.Name) (ref_1 : Lean.Syntax),
  (Lean.Meta.Grind.Origin.stx id ref = Lean.Meta.Grind.Origin.stx id_1 ref_1) = (id = id_1 ∧ ref = ref_1)
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.inl_apply : ∀ {α : Type u_1} {β : Type u_2} (val : α), Function.Embedding.inl val = Sum.inl val
-- Mathlib.Data.Erased
Erased.bind_def : ∀ {α β : Type u_1}, (fun x1 x2 => x1 >>= x2) = Erased.bind
-- Lean.Elab.Command
/-- Return the current scope.  -/
Lean.Elab.Command.getScope : Lean.Elab.Command.CommandElabM Lean.Elab.Command.Scope
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.mkUnder_right : ∀ (R : CommRingCat) (A : Type u) [inst : CommRing A] [inst_1 : Algebra (↑R) A], (R.mkUnder A).right = CommRingCat.of A
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.all_eq_true_iff_forall_contains_getKey_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {p : α → β → Bool},
  m.WF →
    (m.all p = true ↔ ∀ (a : α) (h : m.contains a = true), p (m.getKey a h) (Std.DHashMap.Raw.Const.get m a h) = true)
-- Init.Data.List.Sublist
List.suffix_of_suffix_length_le : ∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <:+ l₃ → l₂ <:+ l₃ → l₁.length ≤ l₂.length → l₁ <:+ l₂
-- Mathlib.Analysis.Fourier.Notation
ContinuousFourier.mk : ∀ {E : Type u_5} {F : outParam (Type u_6)} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace F]
  [inst_2 : FourierTransform E F], Continuous FourierTransform.fourier → ContinuousFourier E F
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_smul : ∀ {R : Type u_1} {S : Type u_2} {a b : R} [inst : SMul S R] (s : S) (z : QuadraticAlgebra R a b), (s • z).re = s • z.re
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.η_comp_tensorDec : ∀ {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 H : CategoryTheory.MonoidalCategory.DayFunctor C V}
  (α :
    CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor ⟶
      (CategoryTheory.MonoidalCategory.tensor C).comp H.functor),
  CategoryTheory.CategoryStruct.comp (F.η G)
      ((CategoryTheory.MonoidalCategory.tensor C).whiskerLeft
        (CategoryTheory.MonoidalCategory.DayFunctor.tensorDesc α).natTrans) =
    α
-- Mathlib.Analysis.Complex.Basic
Complex.ofRealCLM_apply : ∀ (x : ℝ), Complex.ofRealCLM x = ↑x
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.le_isLocal_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  (W : CategoryTheory.MorphismProperty C), W ≤ P.isLocal ↔ P ≤ W.isLocal
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If the additive action of a countable group `G` admits an invariant measure `μ`
with a fundamental domain `s`, then every null-measurable set `t` such that the sets `g +ᵥ t ∩ s`
are pairwise a.e.-disjoint has measure at most `μ s`.  -/
MeasureTheory.IsAddFundamentalDomain.measure_le_of_pairwise_disjoint : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    MeasureTheory.NullMeasurableSet t μ →
      Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun g => (g +ᵥ t) ∩ s) → μ t ≤ μ s
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.support_coeff : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (p : SkewMonoidAlgebra k G), p.coeff.support = p.support
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_dvd_self : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, UniqueFactorizationMonoid.radical a ∣ a
-- Lean.Elab.ConfigEval.Types
_private.Lean.Elab.ConfigEval.Types.0.Lean.Elab.ConfigEval.ReflectConfigItems.mk.inj : ∀ {α : Type} {reflect reflect_1 : α → Lean.Elab.TermElabM (Lean.TSyntaxArray `Lean.Parser.Term.configItem)},
  { reflect := reflect } = { reflect := reflect_1 } → reflect = reflect_1
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.ring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → Ring (CauSeq β abv)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.mem_append_left : ∀ {α : Type u} {s₁ s₂ : Stream'.Seq α} {a : α}, a ∈ s₁ → a ∈ s₁.append s₂
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMul.prod : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_8} [inst : NontriviallyNormedField 𝕜] {E : Type u_9} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_10} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (G : Type u_11)
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Mul G] [ContMDiffMul I n G] {E' : Type u_12}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_13} [inst_10 : TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') (G' : Type u_14) [inst_11 : TopologicalSpace G'] [inst_12 : ChartedSpace H' G']
  [inst_13 : Mul G'] [ContMDiffMul I' n G'], ContMDiffMul (I.prod I') n (G × G')
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
integralClosure.isIntegrallyClosedOfFiniteExtension : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {L : Type u_3} [inst_4 : Field L] [inst_5 : Algebra K L] [inst_6 : Algebra R L] [IsScalarTower R K L] [IsDomain R]
  [FiniteDimensional K L], IsIntegrallyClosed ↥(integralClosure R L)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} [inst_3 : SizeOf C]
  (generators : M.GeneratingSections) (relations : (CategoryTheory.Limits.kernel generators.π).GeneratingSections),
  sizeOf { generators := generators, relations := relations } = 1 + sizeOf generators + sizeOf relations
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharTwoJEqZeroNF.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R),
  W.toCharTwoJEqZeroNF = { u := 1, r := W.a₂, s := 0, t := 0 }
-- Mathlib.Logic.Relation
Relation.EqvGen.brecOn : ∀ {α : Type u_1} {r : α → α → Prop} {motive : (a a_1 : α) → Relation.EqvGen r a a_1 → Prop} {a a_1 : α}
  (t : Relation.EqvGen r a a_1),
  (∀ (a a_2 : α) (t : Relation.EqvGen r a a_2), Relation.EqvGen.below t → motive a a_2 t) → motive a a_1 t
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_toSubtype_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [inst_4 : DecidablePred p] (j : J)
  {Z : C} (h : ⨁ Subtype.restrict p f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p) h) =
    CategoryTheory.CategoryStruct.comp
      (if h : p j then CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0) h
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- The type for paths between two vertices.  -/
SimpleGraph.Path : {V : Type u} → SimpleGraph V → V → V → Type (max 0 u)
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Composing an alternating map with the same linear equiv on each argument gives the zero map
if and only if the alternating map is the zero map.  -/
AlternatingMap.compLinearEquiv_eq_zero_iff : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (f : M [⋀^ι]→ₗ[R] N) (g : M₂ ≃ₗ[R] M), f.compLinearMap ↑g = 0 ↔ f = 0
-- Mathlib.Algebra.Order.Module.Defs
/-- Scalar multiplication on the right by a nonnegative element preserves antitonicity.  -/
Antitone.smul_const : ∀ {α : Type u_1} {β : Type u_2} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
  [SMulPosMono α β] {γ : Type u_3} [inst_5 : Preorder γ] {f : γ → α}, Antitone f → 0 ≤ b → Antitone fun x => f x • b
-- Std.Sat.AIG.If
Std.Sat.AIG.TernaryInput.cast.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α} (input : aig1.TernaryInput)
  (h : aig1.decls.size ≤ aig2.decls.size),
  input.cast h = { discr := input.discr.cast h, lhs := input.lhs.cast h, rhs := input.rhs.cast h }
-- Std.Time.Date.Unit.Month
Std.Time.Month.instReprOffset : Repr Std.Time.Month.Offset
-- Mathlib.Data.ENat.Basic
ENat.top_ne_natCast : ∀ (a : ℕ), ⊤ ≠ ↑a
-- Mathlib.Data.Nat.Choose.Sum
Finset.sum_powerset_neg_one_pow_card_of_nonempty : ∀ {α : Type u_2} {x : Finset α}, x.Nonempty → ∑ m ∈ x.powerset, (-1) ^ m.card = 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeEquivalence.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  CategoryTheory.Limits.Cocone.precomposeEquivalence α =
    CategoryTheory.Equivalence.mk'' (CategoryTheory.Limits.Cocone.precompose α.inv)
      (CategoryTheory.Limits.Cocone.precompose α.hom)
      (CategoryTheory.NatIso.ofComponents'
        (fun s =>
          CategoryTheory.Limits.Cocone.extInv
            (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj s).pt) ⋯)
        ⋯)
      (CategoryTheory.NatIso.ofComponents'
        (fun s =>
          CategoryTheory.Limits.Cocone.extInv
            (CategoryTheory.Iso.refl
              (((CategoryTheory.Limits.Cocone.precompose α.hom).comp
                      (CategoryTheory.Limits.Cocone.precompose α.inv)).obj
                  s).pt)
            ⋯)
        ⋯)
      ⋯
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.instIsMonoidalOppositeOpOpEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.opOpEquivalence C).IsMonoidal
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.instInhabitedPair : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} → (i : ι) → Inhabited (Monoid.PushoutI.NormalWord.Pair d i)
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.instIsAffineFiberOfIsAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] (y : ↥Y),
  AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.Hom.fiber f y)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The tensor product of a pair of algebra morphisms.  -/
Algebra.TensorProduct.map : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        {C : Type uC} →
          {D : Type uD} →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring S] →
                [inst_2 : Algebra R S] →
                  [inst_3 : Semiring A] →
                    [inst_4 : Algebra R A] →
                      [inst_5 : Algebra S A] →
                        [inst_6 : IsScalarTower R S A] →
                          [inst_7 : Semiring B] →
                            [inst_8 : Algebra R B] →
                              [inst_9 : Semiring C] →
                                [inst_10 : Algebra R C] →
                                  [inst_11 : Algebra S C] →
                                    [inst_12 : IsScalarTower R S C] →
                                      [inst_13 : Semiring D] →
                                        [inst_14 : Algebra R D] →
                                          (A →ₐ[S] C) → (B →ₐ[R] D) → TensorProduct R A B →ₐ[S] TensorProduct R C D
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.Rel.rfl_zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  DividedPowerAlgebra.Rel R M 0 0
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinMap.baseChange_tmul : ∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} {N₂ : Type uN₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N₂] [inst_4 : Algebra R A] [inst_5 : Module R M₂]
  [inst_6 : Module R N₂] (B₂ : LinearMap.BilinMap R M₂ N₂) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂),
  ((LinearMap.BilinMap.baseChange A B₂) (a ⊗ₜ[R] m₂)) (a' ⊗ₜ[R] m₂') = (a * a') ⊗ₜ[R] (B₂ m₂) m₂'
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_stepk_cert : ℤ → Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Lean.Declaration
Lean.TheoremVal.mk.inj : ∀ {toConstantVal : Lean.ConstantVal} {value : Lean.Expr} {all : List Lean.Name} {toConstantVal_1 : Lean.ConstantVal}
  {value_1 : Lean.Expr} {all_1 : List Lean.Name},
  { toConstantVal := toConstantVal, value := value, all := all } =
      { toConstantVal := toConstantVal_1, value := value_1, all := all_1 } →
    toConstantVal = toConstantVal_1 ∧ value = value_1 ∧ all = all_1
-- Init.Prelude
/-- Create array `#[a₁, a₂, a₃, a₄, a₅]`  -/
Array.mkArray5 : {α : Type u} → α → α → α → α → α → Array α
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_prod_plift_of_mulSupport_toFinset_subset : ∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M] {f : α → M} (hf : Function.HasFiniteMulSupport (f ∘ PLift.down))
  {s : Finset (PLift α)}, Set.Finite.toFinset hf ⊆ s → ∏ᶠ (i : α), f i = ∏ i ∈ s, f i.down
-- Mathlib.LinearAlgebra.Contraction
map_dualTensorHom : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [inst : CommSemiring R]
  [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 P] [inst_8 : Module R Q] (f : Module.Dual R M) (p : P)
  (g : Module.Dual R N) (q : Q),
  TensorProduct.map ((dualTensorHom R M P) (f ⊗ₜ[R] p)) ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) =
    (dualTensorHom R (TensorProduct R M N) (TensorProduct R P Q))
      ((TensorProduct.dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] (p ⊗ₜ[R] q))
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (e.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (e.inverse.map (CategoryTheory.Functor.OplaxMonoidal.η e.functor)) =
    CategoryTheory.Functor.LaxMonoidal.ε e.inverse
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to a `NonarchAddGroupSeminorm`.  -/
NonarchAddGroupSeminorm.instSMul : {R : Type u_1} →
  {E : Type u_3} →
    [inst : AddGroup E] →
      [inst_1 : SMul R ℝ] → [inst_2 : SMul R NNReal] → [IsScalarTower R NNReal ℝ] → SMul R (NonarchAddGroupSeminorm E)
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- The uniform space isomorphism `ℚ ≃ᵤ ℚ`, where the LHS has the uniformity from
`HeightOneSpectrum.valuation ℚ v` and the RHS has uniformity from
`Rat.padicValuation (natGenerator v)`, for a height-one prime ideal
`v : HeightOneSpectrum R`.  -/
Rat.HeightOneSpectrum.withValEquiv : {R : Type u_2} →
  [inst : CommRing R] →
    [inst_1 : Algebra R ℚ] →
      [inst_2 : IsIntegralClosure R ℤ ℚ] →
        [inst_3 : IsDedekindDomain R] →
          [inst_4 : IsFractionRing R ℚ] →
            (v : IsDedekindDomain.HeightOneSpectrum R) →
              WithVal (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v) ≃ᵤ
                WithVal (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v))
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUInfo.model : Std.Internal.UV.System.CPUInfo → String
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.mk : ℕ →
  Lean.Expr →
    Lean.Level →
      Lean.Expr →
        Lean.Expr →
          Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval →
            Lean.Expr →
              Lean.Expr →
                Option Lean.Expr →
                  Lean.Expr →
                    Lean.Expr →
                      Option Lean.Expr →
                        Option Lean.Expr →
                          Option (Option Lean.Expr) →
                            Option (Option Lean.Expr) →
                              Option (Option Lean.Expr) →
                                Option (Option Lean.Expr) →
                                  Option Lean.Meta.Grind.Arith.Cutsat.ToIntThms →
                                    Option Lean.Meta.Grind.Arith.Cutsat.ToIntThms →
                                      Option (Option Lean.Expr) →
                                        Option (Option Lean.Expr) →
                                          Option (Option Lean.Expr) →
                                            Option (Option Lean.Expr) →
                                              Option (Option Lean.Expr) →
                                                Option (Option Lean.Expr) →
                                                  Option (Option Lean.Expr) → Lean.Meta.Grind.Arith.Cutsat.ToIntInfo
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.interedges_def : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (s t : Finset α),
  G.interedges s t = {e ∈ s ×ˢ t | G.Adj e.1 e.2}
-- Mathlib.NumberTheory.LSeries.Basic
/-- The indicator function of `{1} ⊆ ℕ` with values in `ℂ`.  -/
LSeries.delta : ℕ → ℂ
-- Mathlib.Algebra.Group.Center
Set.zero_mem_addCenter : ∀ {M : Type u_1} [inst : AddZeroClass M], 0 ∈ Set.addCenter M
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addRightMono : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [AddRightMono α], AddRightMono (WithTop α)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.val_inv_toOrderTopSubOnePos_coe : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x : HahnSeries Γ R} (h : 0 < (x - 1).orderTop),
  ↑(↑(HahnSeries.toOrderTopSubOnePos h))⁻¹ = ⋯.unit.inv
-- Mathlib.Order.Heyting.Basic
sdiff_triangle : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a \ c ≤ a \ b ⊔ b \ c
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_of_isEmpty_insertMany : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {l : ρ}, (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).isEmpty = true → (↑m).isEmpty = true
-- Init.Prelude
/-- Implements decidable equality for `List α`, assuming `α` has decidable equality.  -/
List.hasDecEq : {α : Type u} → [DecidableEq α] → (a b : List α) → Decidable (a = b)
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.homRel_iff_rightHomotopyRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.CofibrantObject C} {f g : X ⟶ Y},
  HomotopicalAlgebra.CofibrantObject.homRel C f g ↔ HomotopicalAlgebra.RightHomotopyRel f.hom g.hom
-- Mathlib.Data.Fin.Basic
Fin.mk_eq_one : ∀ {n a : ℕ} {ha : a < n + 2}, ⟨a, ha⟩ = 1 ↔ a = 1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₂_inv_comp_iCycles : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).inv (groupHomology.iCycles A 2) =
    CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.i
      (groupHomology.chainsIso₂ A).inv
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic.0.termX : Lean.ParserDescr
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.getConfig : Lean.Meta.SimpM Lean.Meta.Simp.Config