mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.aemeasurable_withDensity_ennreal_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → NNReal},
  Measurable f →
    ∀ {g : α → ENNReal}, AEMeasurable g (μ.withDensity fun x => ↑(f x)) ↔ AEMeasurable (fun x => ↑(f x) * g x) μ
-- Mathlib.Data.Multiset.ZeroCons
Multiset.notMem_zero : ∀ {α : Type u_1} (a : α), a ∉ 0
-- Mathlib.CategoryTheory.Shift.CommShift
/-- For any functor `F : C ⥤ D` and any `a` in `A` such that `a = 0`,
this is the obvious isomorphism `shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` deduced from the
isomorphisms `shiftFunctorZero'` on both categories `C` and `D`.  -/
CategoryTheory.Functor.CommShift.isoZero' : {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] →
        (F : CategoryTheory.Functor C D) →
          (A : Type u_4) →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  (a : A) →
                    a = 0 → ((CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.faithful_of_comp_essSurj : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor D E) (L : CategoryTheory.Functor C D) [L.EssSurj],
  (∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g) → F.Faithful
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
AddMonoidAlgebra.cardinalMk_of_fintype : ∀ (R M : Type u) [inst : Semiring R] [inst_1 : Fintype M],
  Cardinal.mk (AddMonoidAlgebra R M) = Cardinal.mk R ^ Fintype.card M
-- Mathlib.Analysis.Analytic.Composition
/-- When `a` is a composition of `n` and `b` is a composition of `a.length`, `a.gather b` is the
composition of `n` obtained by gathering all the blocks of `a` corresponding to a block of `b`.
For instance, if `a = [6, 5, 3, 5, 2]` and `b = [2, 3]`, one should gather together
the first two blocks of `a` and its last three blocks, giving `a.gather b = [11, 10]`.  -/
Composition.gather : {n : ℕ} → (a : Composition n) → Composition a.length → Composition n
-- Mathlib.Data.Set.Finite.Basic
instWellFoundedLTSubtypeSetFinite : ∀ {α : Type u}, WellFoundedLT { s // s.Finite }
-- Mathlib.Data.Finsupp.Weight
Finsupp.nsmul_single_one_image : ∀ {α : Type u_5} {n : ℕ} {s : Set α}, n • (fun x => fun₀ | x => 1) '' s = {x | Finsupp.degree x = n ∧ ↑x.support ⊆ s}
-- Mathlib.SetTheory.Ordinal.Enum
/-- If `s` is closed under nonempty suprema, then its enumerator function is normal.
See also `enumOrd_isNormal_iff_isClosed`.  -/
Ordinal.isNormal_enumOrd : ∀ {s : Set Ordinal.{u}},
  (∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s) → ¬BddAbove s → Order.IsNormal (Ordinal.enumOrd s)
-- Mathlib.RepresentationTheory.Invariants
/-- The invariants of the representation `linHom ρ σ` correspond to intertwining maps
from `ρ` to `σ`.  -/
Representation.invariantsEquivIntertwiningMap : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommRing k] →
          [inst_1 : Group G] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : Module k V] →
                [inst_4 : AddCommGroup W] →
                  [inst_5 : Module k W] →
                    (ρ : Representation k G V) →
                      (σ : Representation k G W) → ↥(ρ.linHom σ).invariants ≃ₗ[k] ρ.IntertwiningMap σ
-- Mathlib.RingTheory.Regular.Category
ModuleCat.smulShortComplex_g_epi : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) (r : R), CategoryTheory.Epi (M.smulShortComplex r).g
-- Std.Time.Format.Basic
Std.Time.TypeFormat : Std.Time.Modifier → Type
-- Mathlib.Algebra.GradedMonoid
SetLike.list_prod_map_mem_graded : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Monoid R] [inst_2 : AddMonoid ι]
  {A : ι → S} [SetLike.GradedMonoid A] {ι' : Type u_4} (l : List ι') (i : ι' → ι) (r : ι' → R),
  (∀ j ∈ l, r j ∈ A (i j)) → (List.map r l).prod ∈ A (List.map i l).sum
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.mk_ι_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W)
  (inr : Z ⟶ W) (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr),
  (CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app CategoryTheory.Limits.WalkingSpan.left = inl
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.ext : ∀ (A : Type uA) [inst : AddCommGroup A] {c c' : CharacterModule A}, (∀ (x : A), c x = c' x) → c = c'
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.neg_sup : ∀ {G : Type u_2} [inst : AddGroup G] (S T : AddSubmonoid G), -(S ⊔ T) = -S ⊔ -T
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.toDigitsCore.match_1.eq_2 : ∀ (motive : ℕ → ℕ → List Char → Sort u_1) (fuel n : ℕ) (ds : List Char)
  (h_1 : (x : ℕ) → (ds : List Char) → motive 0 x ds) (h_2 : (fuel n : ℕ) → (ds : List Char) → motive fuel.succ n ds),
  (match fuel.succ, n, ds with
    | 0, x, ds => h_1 x ds
    | fuel.succ, n, ds => h_2 fuel n ds) =
    h_2 fuel n ds
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT)
  [AlgebraicGeometry.Flat f],
  AlgebraicGeometry.IsAffineOpen US →
    IsCompact ↑UT →
      IsCompact ↑UX →
        (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE iX US UX hUSX)).Flat →
          CategoryTheory.Mono (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.State.numCalls : Lean.Util.ParamMinimizer.State✝ → ℕ
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicField.instSMulOfAlgebra : (n : ℕ) →
  (A : Type u_1) →
    (K : Type u_2) → [inst : CommRing A] → [inst_1 : Field K] → [Algebra A K] → SMul A (CyclotomicField n K)
-- Batteries.Data.List.Lemmas
List.IsChain.getElem : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.IsChain R l → ∀ (i : ℕ) (hi : i + 1 < l.length), R l[i] l[i + 1]
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive]
  (α : F ⟶ G) {X : C} (P : CategoryTheory.InjectiveResolution X),
  (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α).app X =
    CategoryTheory.CategoryStruct.comp (P.isoRightDerivedToHomotopyCategoryObj F).hom
      (CategoryTheory.CategoryStruct.comp
        ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex))
        (P.isoRightDerivedToHomotopyCategoryObj G).inv)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.instIsComonHomHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} (f : M ⟶ N), CategoryTheory.IsComonHom f.hom
-- Mathlib.Order.Grade
grade_eq_grade_iff : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : LinearOrder α] [inst_2 : GradeOrder 𝕆 α] {a b : α},
  grade 𝕆 a = grade 𝕆 b ↔ a = b
-- Mathlib.Order.Filter.Pi
Filter.map_pi_map_coprodᵢ_le : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {β : ι → Type u_3} {m : (i : ι) → α i → β i},
  Filter.map (fun k i => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun i => Filter.map (m i) (f i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos.eq_1 : ∀ (x : ℝ), Real.arccos x = Real.pi / 2 - Real.arcsin x
-- Lean.Meta.Tactic.SolveByElim
/-- The default `maxDepth` for `apply_rules` is higher.  -/
Lean.Meta.SolveByElim.ApplyRulesConfig : Type
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} [inst_2 : Inhabited (β k')],
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (Std.ExtDTreeMap.ofList l cmp).get! k' = cast ⋯ v
-- Mathlib.Algebra.Free
FreeAddSemigroup.of_tail : ∀ {α : Type u} (x : α), (FreeAddSemigroup.of x).tail = []
-- Batteries.Linter.UnnecessarySeqFocus
/-- True if this is a `<;>` node in either `tactic` or `conv` classes.  -/
Batteries.Linter.UnnecessarySeqFocus.isSeqFocus : Lean.SyntaxNodeKind → Bool
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_zero : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n], Matrix.num 0 = 0
-- Mathlib.Lean.Meta
/-- Applies `intro` repeatedly until it fails. We use this instead of
`Lean.MVarId.intros` to allowing unfolding.
For example, if we want to do introductions for propositions like `¬p`,
the `¬` needs to be unfolded into `→ False`, and `intros` does not do such unfolding.  -/
Lean.MVarId.intros! : Lean.MVarId → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Lean.Elab.DeprecatedSyntax
/-- Check whether `stx` is a deprecated syntax kind, and if so, emit a warning.

If `macroStack` is non-empty, the warning is attributed to the macro call site rather than the
syntax itself.
 -/
Lean.Elab.checkDeprecatedSyntax : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadLog m] →
        [Lean.MonadOptions m] →
          [Lean.AddMessageContext m] → [Lean.MonadRef m] → Lean.Syntax → Lean.Elab.MacroStack → m Unit
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isNone_getElem?_toArray_rco_eq : ∀ {m n : ℤ} {i : ℕ}, ((m...n).toArray[i]?.isNone = true) = ((n - m).toNat ≤ i)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonDidOpenTextDocumentParams.toJson : Lean.Lsp.DidOpenTextDocumentParams → Lean.Json
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k} (h : ModuleCat.of k ↑B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ 0)
      (CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).hom
      (CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom φ) h)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Iic_of_tendsto_atBot_atBot : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R],
  Filter.Tendsto (↑f) Filter.atBot Filter.atBot → ∀ (x : R), f.measure (Set.Iic x) = ⊤
-- Lean.Message
Lean.termM!_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.instIsAddModHomId : ∀ {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.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.AddMonObj A] {M : D} [inst_5 : CategoryTheory.AddModObj A M],
  CategoryTheory.IsAddModHom A (CategoryTheory.CategoryStruct.id M)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The difference of two `C^n` functions within a set at a point is `C^n` within this set
at this point.  -/
ContDiffWithinAt.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {n : WithTop ℕ∞} {s : Set E} {f g : E → F},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n (fun x => f x - g x) s x
-- Mathlib.Order.Filter.Basic
/-- Eta-expanded form of `Filter.EventuallyEq.mul` -/
Filter.EventuallyEq.fun_mul : ∀ {α : Type u} {β : Type v} [inst : Mul β] {f f' g g' : α → β} {l : Filter α},
  f =ᶠ[l] g → f' =ᶠ[l] g' → (fun i => f i * f' i) =ᶠ[l] fun i => g i * g' i
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.verts_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.toSubgraph.verts = {w | w ∈ p.support}
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.mul_of_associated : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x z : R)
  (y : S) [IsLocalization.Away x S] {T : Type u_4} [inst_4 : CommRing T] [inst_5 : Algebra S T] [inst_6 : Algebra R T]
  [IsScalarTower R S T] [IsLocalization.Away y T], Associated ((algebraMap R S) z) y → IsLocalization.Away (x * z) T
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
/-- Unfold `birdDet` at a successor dimension.  -/
BirdDet.birdDet_succ : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (A : Array R),
  BirdDet.birdDet (k + 1) A = (-1) ^ k * (BirdDet.stepEntry (k + 1) A)^[k] (BirdDet.get (k + 1) A) 0 0
-- Mathlib.Topology.UniformSpace.Defs
Filter.HasBasis.biInter_biUnion_ball : ∀ {α : Type ua} {ι : Sort u_1} [inst : UniformSpace α] {p : ι → Prop} {U : ι → SetRel α α},
  (uniformity α).HasBasis p U → ∀ (s : Set α), ⋂ i, ⋂ (_ : p i), ⋃ x ∈ s, UniformSpace.ball x (U i) = closure s
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.CongrInfo.fixedPrefix.injEq : ∀ (prefixSize suffixSize prefixSize_1 suffixSize_1 : ℕ),
  (Lean.Meta.Sym.CongrInfo.fixedPrefix prefixSize suffixSize =
      Lean.Meta.Sym.CongrInfo.fixedPrefix prefixSize_1 suffixSize_1) =
    (prefixSize = prefixSize_1 ∧ suffixSize = suffixSize_1)
-- Mathlib.Data.Int.Cast.Defs
/-- The canonical map `ℕ → R` is a homomorphism.  -/
AddCommGroupWithOne.natCast_succ : ∀ {R : Type u} [self : AddCommGroupWithOne R] (n : ℕ), ↑(n + 1) = ↑n + 1
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.inv_iff : ∀ {G : Type u_3} [inst : DivisionCommMonoid G] {k : ℕ} {ζ : G}, IsPrimitiveRoot ζ⁻¹ k ↔ IsPrimitiveRoot ζ k
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- Given a linearly ordered family `v` of vectors of `M` and a natural number `n`, produce the
family of `n`fold exterior products of elements of `v`, seen as members of the
`n`th exterior power.  -/
exteriorPower.ιMulti_family : (R : Type u) →
  [inst : CommRing R] →
    (n : ℕ) →
      {M : Type u_1} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → {I : Type u_4} → [LinearOrder I] → (I → M) → ↑(Set.powersetCard I n) → ↥(⋀[R]^n M)
-- Init.Data.BitVec.Bootstrap
BitVec.toNat_ofFin : ∀ {n : ℕ} (x : Fin (2 ^ n)), { toFin := x }.toNat = ↑x
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.directive.withIndentColumn : ℕ → (ℕ → Lean.Parser.ParserFn) → Lean.Parser.ParserFn
-- Mathlib.Data.Complex.Basic
Complex.instNeg : Neg ℂ
-- Mathlib.Data.Set.Prod
Set.offDiag_mono : ∀ {α : Type u_1}, Monotone Set.offDiag
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.lambdaTelescopeImp.process : {α : Type} →
  Bool →
    Bool →
      Option ℕ →
        (Array Lean.Expr → Lean.Expr → Lean.MetaM α) →
          Bool → Bool → Bool → Lean.LocalContext → Array Lean.Expr → Lean.Expr → Lean.MetaM α
-- Mathlib.RingTheory.PowerSeries.CoeffMulMem
PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal' : ∀ {A : Type u_1} [inst : Semiring A] {I : Ideal A} {f g : PowerSeries A},
  (∀ (i : ℕ), (PowerSeries.coeff i) g ∈ I) → ∀ (i : ℕ), (PowerSeries.coeff i) (f * g) ∈ I
-- Mathlib.LinearAlgebra.Multilinear.TensorProduct
/-- A more bundled version of `MultilinearMap.domCoprodDep`, as a linear map
from the tensor product of spaces of multilinear maps.  -/
MultilinearMap.domCoprodDep' : {R : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      [inst : CommSemiring R] →
        {N₁ : Type u_6} →
          [inst_1 : AddCommMonoid N₁] →
            [inst_2 : Module R N₁] →
              {N₂ : Type u_7} →
                [inst_3 : AddCommMonoid N₂] →
                  [inst_4 : Module R N₂] →
                    {N : ι₁ ⊕ ι₂ → Type u_8} →
                      [inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)] →
                        [inst_6 : (i : ι₁ ⊕ ι₂) → Module R (N i)] →
                          TensorProduct R (MultilinearMap R (fun i₁ => N (Sum.inl i₁)) N₁)
                              (MultilinearMap R (fun i₂ => N (Sum.inr i₂)) N₂) →ₗ[R]
                            MultilinearMap R N (TensorProduct R N₁ N₂)
-- Init.System.IO
/-- The file should be opened for writing.

If the file already exists, it is truncated to zero length. Otherwise, a new file is created. The
read/write cursor is positioned at the beginning of the file.

* `open` flags: `O_WRONLY | O_CREAT | O_TRUNC`
* `fdopen` mode: `w`
 -/
IO.FS.Mode.write : IO.FS.Mode
-- Mathlib.Topology.Separation.CountableSeparatingOn
/-- If `X` is a topological space, `s` is a set in `X` such that the induced topology is T₀ and is
second countable, then there exists a countable family of open sets in `X` that separates points
of `s`.  -/
instHasCountableSeparatingOnIsOpenOfT0SpaceOfSecondCountableTopologyElem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [T0Space ↑s] [SecondCountableTopology ↑s],
  HasCountableSeparatingOn X IsOpen s
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.forget_map : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (P : CategoryTheory.MorphismProperty T)
  (Q : CategoryTheory.MorphismProperty A) (W : CategoryTheory.MorphismProperty B) [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X ⟶ Y),
  (CategoryTheory.MorphismProperty.Comma.forget L R P Q W).map f = CategoryTheory.MorphismProperty.Comma.Hom.hom f
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.mk.injEq : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (ringInst semiringInst : Lean.Expr) (charInst? : Option (Lean.Expr × ℕ))
  (addFn? mulFn? subFn? negFn? powFn? intCastFn? natCastFn? one? : Option Lean.Expr) (id_1 : ℕ) (type_1 : Lean.Expr)
  (u_1 : Lean.Level) (ringInst_1 semiringInst_1 : Lean.Expr) (charInst?_1 : Option (Lean.Expr × ℕ))
  (addFn?_1 mulFn?_1 subFn?_1 negFn?_1 powFn?_1 intCastFn?_1 natCastFn?_1 one?_1 : Option Lean.Expr),
  ({ id := id, type := type, u := u, ringInst := ringInst, semiringInst := semiringInst, charInst? := charInst?,
        addFn? := addFn?, mulFn? := mulFn?, subFn? := subFn?, negFn? := negFn?, powFn? := powFn?,
        intCastFn? := intCastFn?, natCastFn? := natCastFn?, one? := one? } =
      { id := id_1, type := type_1, u := u_1, ringInst := ringInst_1, semiringInst := semiringInst_1,
        charInst? := charInst?_1, addFn? := addFn?_1, mulFn? := mulFn?_1, subFn? := subFn?_1, negFn? := negFn?_1,
        powFn? := powFn?_1, intCastFn? := intCastFn?_1, natCastFn? := natCastFn?_1, one? := one?_1 }) =
    (id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          ringInst = ringInst_1 ∧
            semiringInst = semiringInst_1 ∧
              charInst? = charInst?_1 ∧
                addFn? = addFn?_1 ∧
                  mulFn? = mulFn?_1 ∧
                    subFn? = subFn?_1 ∧
                      negFn? = negFn?_1 ∧
                        powFn? = powFn?_1 ∧ intCastFn? = intCastFn?_1 ∧ natCastFn? = natCastFn?_1 ∧ one? = one?_1)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_right_hom : ∀ {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 D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G)
  (g : CategoryTheory.StructuredArrow f.right F),
  ((CategoryTheory.StructuredArrow.preEquivalenceInverse F f).obj g).right.hom =
    CategoryTheory.CategoryStruct.comp f.hom (G.map g.hom)
-- Plausible.Testable
Plausible.False.printableProp : Plausible.PrintableProp False
-- Mathlib.Data.List.AList
AList.ext : ∀ {α : Type u} {β : α → Type v} {s t : AList β}, s.entries = t.entries → s = t
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.mkSet : (self : ShareCommon.StateFactoryBuilder) → {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → self.Set α
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.coconeOfCoconeUncurry_ι_app : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCocones F}
  (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j))
  (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.uncurry.obj F)) (j : J),
  (CategoryTheory.Limits.coconeOfCoconeUncurry Q c).ι.app j =
    (Q j).desc { pt := c.pt, ι := { app := fun k => c.ι.app (j, k), naturality := ⋯ } }
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_apply : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [inst : Inner ℝ E] (t : E),
  MeasureTheory.charFun μ t = ∫ (x : E), Complex.exp (↑(inner ℝ x t) * Complex.I) ∂μ
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.coe_pow : ∀ {K : Type u_1} [inst : Field K] (x : (NumberField.RingOfIntegers K)ˣ) (n : ℕ),
  (algebraMap (NumberField.RingOfIntegers K) K) ↑(x ^ n) = (algebraMap (NumberField.RingOfIntegers K) K) ↑x ^ n
-- Aesop.Script.SScript
Aesop.Script.SScript.empty.sizeOf_spec : sizeOf Aesop.Script.SScript.empty = 1
-- Mathlib.Data.Set.Function
Set.surjOn_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {p : Set γ} {f : α → β} {g : β → γ},
  Set.SurjOn (g ∘ f) s p ↔ Set.SurjOn g (f '' s) p
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k : α},
  (Std.ExtTreeMap.unitOfList l cmp)[k]! = ()
-- Mathlib.Data.Multiset.Sum
Multiset.map_disjSum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Multiset α} {t : Multiset β} (f : α ⊕ β → γ),
  Multiset.map f (s.disjSum t) = Multiset.map (fun x => f (Sum.inl x)) s + Multiset.map (fun x => f (Sum.inr x)) t
-- Mathlib.Data.Nat.MaxPowDiv
padicValNat_base_pow : ∀ {p : ℕ}, 1 < p → ∀ (k : ℕ), padicValNat p (p ^ k) = k
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableSMul_iterateMulAct : ∀ {α : Type u_2} {x : MeasurableSpace α} {f : α → α}, MeasurableSMul (IterateMulAct f) α ↔ Measurable f