mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.productiveRel_of_inner : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [inst : Std.Iterator α m β]
  [inst_1 : Std.Iterators.Productive α m] {remaining : ℕ} {it it' : Std.IterM m β},
  it'.finitelyManySkips.Rel it.finitelyManySkips →
    Std.Iterators.Types.Drop.ProductiveRel✝ m (Std.IterM.drop remaining it') (Std.IterM.drop remaining it)
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.mk.sizeOf_spec : ∀ {R : Type u} [inst : Ring R] [inst_1 : SizeOf R] (n : ℕ) (S : Submodule R (Fin n → R)),
  sizeOf { n := n, S := S } = 1 + sizeOf n + sizeOf S
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.star_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (X_1 : C), ((CategoryTheory.Over.star X).obj X_1).left = (X ⨯ X_1)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_le_prod_of_ne_one' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [CanonicallyOrderedMul M] {f : ι → M}
  {s t : Finset ι}, (∀ x ∈ s, f x ≠ 1 → x ∈ t) → ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mapsTo_smul_orbit : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] (m : M) (a : α),
  Set.MapsTo (fun x => m • x) (MulAction.orbit M a) (MulAction.orbit M a)
-- Mathlib.Data.Set.Prod
Set.preimage_coe_coe_diagonal : ∀ {α : Type u_1} (s : Set α), (Prod.map (fun x => ↑x) fun x => ↑x) ⁻¹' Set.diagonal α = Set.diagonal ↑s
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The vector space of functions on a `Fintype ι` has `finrank` equal to the cardinality of `ι`.  -/
Module.finrank_fintype_fun_eq_card : ∀ (R : Type u) {η : Type u₁'} [inst : Semiring R] [StrongRankCondition R] [inst_2 : Fintype η],
  Module.finrank R (η → R) = Fintype.card η
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquivAlgOfEq_coe_eq_factor : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (h : I = J),
  ↑(Ideal.quotientEquivAlgOfEq R₁ h) = Ideal.Quotient.factor ⋯
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mem_nonZeroDivisors_iff : ∀ {R : Type u} [inst : CommSemiring R] {P : Polynomial R},
  P ∈ nonZeroDivisors (Polynomial R) ↔ ∀ (a : R), a • P = 0 → a = 0
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.univ : ∀ {M : Type u_1} [inst : AddCommMonoid M] [AddMonoid.FG M], IsSemilinearSet Set.univ
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangle_obj₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), h.triangle.obj₁ = Z₁₂
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.insertListₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  Std.DHashMap.Internal.Raw₀.Const.insertListₘ m [] = m
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Expression of `circleAverage` with arbitrary center in terms of `circleAverage` with center zero.
 -/
Real.circleAverage_map_add_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  Real.circleAverage (fun z => f (z + c)) 0 R = Real.circleAverage f c R
-- Init.Internal.Order.Basic
Lean.Order.lfp_prefixed : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] {f : α → α} {hm : Lean.Order.monotone f},
  Lean.Order.PartialOrder.rel (f (Lean.Order.lfp f)) (Lean.Order.lfp f)
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.getUnlintedRanges.match_3.splitter : (motive : Std.HashSet Lean.Syntax.Range → Lean.Syntax → Sort u_1) →
  (x : Std.HashSet Lean.Syntax.Range) →
    (x_1 : Lean.Syntax) →
      ((curr : Std.HashSet Lean.Syntax.Range) →
          (info : Lean.SourceInfo) →
            (kind : Lean.SyntaxNodeKind) → (args : Array Lean.Syntax) → motive curr (Lean.Syntax.node info kind args)) →
        ((curr : Std.HashSet Lean.Syntax.Range) →
            (info : Lean.SourceInfo) → motive curr (Lean.Syntax.atom info "where")) →
          ((curr : Std.HashSet Lean.Syntax.Range) →
              (x : Lean.Syntax) →
                (∀ (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax),
                    x = Lean.Syntax.node info kind args → False) →
                  (∀ (info : Lean.SourceInfo), x = Lean.Syntax.atom info "where" → False) → motive curr x) →
            motive x x_1
-- Mathlib.RingTheory.Ideal.UFD
/-- Let `R` be a Noetherian domain. Then `R` is a UFD if and only if every height `1` prime ideal is
principal.  -/
UniqueFactorizationMonoid.iff_forall_isPrincipal_of_height_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsNoetherianRing R],
  UniqueFactorizationMonoid R ↔ ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.congr : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb →
    ∀ {f' : α → β}, Measurable f' → f =ᵐ[μa] f' → MeasureTheory.Measure.QuasiMeasurePreserving f' μa μb
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_lt_add_iff_left : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [inst_1 : LT α] [AddLeftStrictMono α] [AddLeftReflectLT α],
  x ≠ ⊥ → (x + y < x + z ↔ y < z)
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap_wrap : ∀ (i : Lean.Grind.IntInterval) (x : ℤ), i.wrap (i.wrap x) = i.wrap x
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.const_abs : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : AddCommGroup β] [inst_1 : LinearOrder β] (x : β), ↑|x| = |↑x|
-- Lean.DocString.Types
Lean.Doc.Inline.bold.sizeOf_spec : ∀ {i : Type u} [inst : SizeOf i] (content : Array (Lean.Doc.Inline i)),
  sizeOf (Lean.Doc.Inline.bold content) = 1 + sizeOf content
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- **Alias** of the forward direction of `memℓp_norm_iff`. -/
Memℓp.of_norm : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  Memℓp (fun x => ‖f x‖) p → Memℓp f p
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_f : ∀ {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.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_3),
  (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f =
    CategoryTheory.CategoryStruct.comp ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂))
      (X.pOpcycles f₁₂ f₃ n₁)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Given two coforks with isomorphic components in such a way that the natural diagrams commute, then
if one is a colimit, then the other one is as well.
 -/
CategoryTheory.Limits.Cofork.isColimitOfIsos : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {X' Y' : C} →
          (c : CategoryTheory.Limits.Cofork f g) →
            CategoryTheory.Limits.IsColimit c →
              {f' g' : X' ⟶ Y'} →
                (c' : CategoryTheory.Limits.Cofork f' g') →
                  (e₀ : X ≅ X') →
                    (e₁ : Y ≅ Y') →
                      (e : c.pt ≅ c'.pt) →
                        autoParam
                            (CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom)
                            CategoryTheory.Limits.Cofork.isColimitOfIsos._auto_1 →
                          autoParam
                              (CategoryTheory.CategoryStruct.comp e₀.hom g' =
                                CategoryTheory.CategoryStruct.comp g e₁.hom)
                              CategoryTheory.Limits.Cofork.isColimitOfIsos._auto_3 →
                            autoParam
                                (CategoryTheory.CategoryStruct.comp e₁.inv
                                    (CategoryTheory.CategoryStruct.comp c.π e.hom) =
                                  c'.π)
                                CategoryTheory.Limits.Cofork.isColimitOfIsos._auto_5 →
                              CategoryTheory.Limits.IsColimit c'
-- Batteries.Data.List.Lemmas
List.findIdxs.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (start : ℕ),
  List.findIdxs p l start = List.foldrIdx (fun i a is => bif p a then i :: is else is) [] l start
-- Mathlib.GroupTheory.Coset.Basic
leftAddCosetEquivalence_rel : ∀ {α : Type u_1} [inst : Add α] (s : Set α), Equivalence (LeftAddCosetEquivalence s)
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_symm_apply_mk_tmul : ∀ {R : Type u_1} (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] (M : Type u_4) [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : Module A M] [inst_8 : IsScalarTower R A M] {N : Type u_5} [inst_9 : AddCommGroup N] [inst_10 : Module R N]
  [inst_11 : Module B N] [inst_12 : IsScalarTower R B N] (n : Submodule B N) (x : M) (y : N),
  (TensorProduct.AlgebraTensorModule.tensorQuotientEquiv A B M n).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) =
    x ⊗ₜ[R] Submodule.Quotient.mk y
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.ext : ∀ {α : Type w} {x y : Std.Iterators.Types.ListIterator α}, x.list = y.list → x = y
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.rightUnitor_hom_out_app : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C),
  (CategoryTheory.EnrichedCat.rightUnitor F).hom.out.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressEnd.mk : String → Option String → Lean.Lsp.WorkDoneProgressEnd
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Constructor for `Equivalence.CommShift`.  -/
CategoryTheory.Equivalence.CommShift.mk'' : ∀ {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] (E : C ≌ D) (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : E.functor.CommShift A]
  [inst_6 : E.inverse.CommShift A], CategoryTheory.NatTrans.CommShift E.counitIso.hom A → E.CommShift A
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedSolverExtensionState : Inhabited Lean.Meta.Grind.SolverExtensionState
-- Init.Data.List.Lemmas
List.filterMap_replicate_of_some : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : ℕ} {f : α → Option β},
  f a = some b → List.filterMap f (List.replicate n a) = List.replicate n b
-- Lean.Util.MonadCache
Lean.MonadCacheT.instMonadControl : {ω α β : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] → [inst_1 : BEq α] → [inst_2 : Hashable α] → MonadControl m (Lean.MonadCacheT α β m)
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The `GoodProducts` in `C` that contain `o` (they necessarily start with `o`, see
`GoodProducts.head!_eq_o_of_maxProducts`)
 -/
Profinite.NobelingProof.GoodProducts.MaxProducts : {I : Type u} →
  Set (I → Bool) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} → (o < Ordinal.type fun x1 x2 => x1 < x2) → Set (Profinite.NobelingProof.Products I)
-- Mathlib.RingTheory.PicardGroup
Submodule.projective_units : ∀ {R : Type u} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  (I : (Submodule R A)ˣ), Module.Projective R ↥↑I
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
/-- If a continuous real-linear functional is bounded by a `𝕜`-seminorm, then its `𝕜`-linear
extension is bounded by the same seminorm.  -/
StrongDual.norm_extendRCLike_le_seminorm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : Module ℝ E]
  [inst_4 : IsScalarTower ℝ 𝕜 E] [inst_5 : TopologicalSpace E] [inst_6 : ContinuousConstSMul 𝕜 E] (fr : StrongDual ℝ E)
  {p : Seminorm 𝕜 E}, (∀ (x : E), |fr x| ≤ p x) → ∀ (x : E), ‖fr.extendRCLike x‖ ≤ p x
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_div_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : Div Z] [inst_4 : ContinuousDiv Z] (f g : C(X × Y, Z)) (x : X),
  (f / g).curry x = f.curry x / g.curry x
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.Reason.no.sizeOf_spec : sizeOf Std.Time.Reason.no✝ = 1
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.proper.inj : ∀ {s needle : String.Slice} {table : Vector ℕ needle.utf8ByteSize}
  {ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle} {stackPos needlePos : String.Pos.Raw}
  {hn : needlePos < needle.rawEndPos} {needle_1 : String.Slice} {table_1 : Vector ℕ needle_1.utf8ByteSize}
  {ht_1 : table_1 = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle_1}
  {stackPos_1 needlePos_1 : String.Pos.Raw} {hn_1 : needlePos_1 < needle_1.rawEndPos},
  String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =
      String.Slice.Pattern.ForwardSliceSearcher.proper needle_1 table_1 ht_1 stackPos_1 needlePos_1 hn_1 →
    needle = needle_1 ∧ table ≍ table_1 ∧ stackPos = stackPos_1 ∧ needlePos = needlePos_1
-- Mathlib.Data.Finset.Erase
Finset.erase_eq_self : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, s.erase a = s ↔ a ∉ s
-- Mathlib.Logic.Equiv.Defs
/-- `Equiv.symm` defines an equivalence between `α ≃ β` and `β ≃ α`.  -/
Equiv.symmEquiv : (α : Sort u_1) → (β : Sort u_2) → α ≃ β ≃ (β ≃ α)
-- Std.Data.String.ToNat
Nat.isNat_repr : ∀ (n : ℕ), n.repr.isNat = true
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.toOuterMeasure_map_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (p : PMF α) (s : Set β),
  (PMF.map f p).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addDysonETransform.card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addDysonETransform e x).1.card + (Finset.addDysonETransform e x).2.card = x.1.card + x.2.card
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Right whiskering for morphisms  -/
CategoryTheory.Bicategory.whiskerRight : {B : Type u} →
  [self : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f g : a ⟶ b} →
        (f ⟶ g) → (h : b ⟶ c) → CategoryTheory.CategoryStruct.comp f h ⟶ CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Order.Interval.Set.Infinite
Set.Ioo_infinite : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] {a b : α}, a < b → (Set.Ioo a b).Infinite
-- Mathlib.Data.ENat.Pow
ENat.epow_pos : ∀ {x y : ℕ∞}, x ≠ 0 → 0 < x ^ y
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedComp_π_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] (j : J) {Z : V}
  (h : ((CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₃).obj (Opposite.op j)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₃) j) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₂) j)
        (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₂ F₃) j))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j)) h)
-- Mathlib.Algebra.Module.Presentation.Differentials
Algebra.Presentation.differentialsRelations.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ),
  pres.differentialsRelations =
    { G := ι, R := σ,
      relation := fun r =>
        Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
          ((KaehlerDifferential.mvPolynomialBasis R ι).repr
            ((KaehlerDifferential.D R (MvPolynomial ι R)) (pres.relation r))) }
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Given a functor `F` and an equivalence of categories `e` such that `e.inverse` and `F ⋙ e.functor`
are monoidal functors, `F` is monoidal as well.
 -/
CategoryTheory.Equivalence.monoidalOfPostcompFunctor : {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 : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (e : C ≌ D) →
                    (F : CategoryTheory.Functor E C) →
                      {F' : CategoryTheory.Functor E D} →
                        (F.comp e.functor ≅ F') → [e.inverse.Monoidal] → [F'.Monoidal] → F.Monoidal
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.PredTrans.pushOption.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Types and type formers are mostly ignored during E-matching, and processed using
`isDefEq`. However, if the argument is of the form `C ..` where `C` is inductive type
we process it as part of the pattern. Suppose we have `as bs : List α`, and a pattern
candidate expression `as ++ bs`, i.e., `@HAppend.hAppend (List α) (List α) (List α) inst as bs`.
If we completely ignore the types, the pattern will just be
```
@HAppend.hAppend _ _ _ _ #1 #0
```
This is not ideal because the E-matcher will try it in any goal that contains `++`,
even if it does not even mention lists.
 -/
Lean.Meta.Grind.NormalizePattern.PatternArgKind.typeFormer : Lean.Meta.Grind.NormalizePattern.PatternArgKind
-- Lean.Elab.DocString
/-- Registers a single `MVarErrorInfo` so that, if any metavariable in `e` remains unresolved at the
end of document elaboration, one error is emitted at `ref` naming the documentation `extension` (the
constant implementing the role/code block, e.g. `Lean.Doc.given`) and the supplied `location`
(e.g. "type of variable `xs`") that contained the hole. The element name is rendered via
`docElementMessage`. Roles and code blocks use this to attach a diagnostic to the syntax
that introduced the variable, in addition to the standard placeholder errors that the underlying
elaborator emits for unsolved metas.
 -/
Lean.Doc.registerDocMVar : Lean.Name → Lean.Expr → Lean.Syntax → Lean.MessageData → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- A precoverage has pullbacks, if every covering presieve has pullbacks along arbitrary
morphisms.  -/
CategoryTheory.Precoverage.HasPullbacks : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → Prop
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndepOn_iUnion_of_directed : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {η : Type u_6} {s : η → Set ι},
  Directed (fun x1 x2 => x1 ⊆ x2) s → (∀ (i : η), LinearIndepOn R v (s i)) → LinearIndepOn R v (⋃ i, s i)
-- Mathlib.Algebra.Group.Prod
Prod.instDivisionMonoid : {G : Type u_1} → {H : Type u_2} → [DivisionMonoid G] → [DivisionMonoid H] → DivisionMonoid (G × H)
-- Mathlib.Data.EReal.Inv
EReal.zero_div : ∀ {a : EReal}, 0 / a = 0
-- Mathlib.Order.Max
not_isTop : ∀ {α : Type u_1} [inst : LE α] [NoTopOrder α] (a : α), ¬IsTop a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.eraseKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α), Std.Internal.List.eraseKey k [] = []
-- Mathlib.Topology.Sets.Closeds
/-- in a `T1Space`, coatoms of `TopologicalSpace.Opens α` are precisely complements of singletons:
`({x} : Closeds α).compl`.  -/
TopologicalSpace.Opens.isCoatom_iff : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {s : TopologicalSpace.Opens α},
  IsCoatom s ↔ ∃ x, s = {x}.compl
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceVal : Lean.Meta.Simp.DSimproc
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_mono_of_forall_exists' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {ι' : Sort u_5} {f : ι → α} {g : ι' → α},
  BddAbove (Set.range g) → (∀ (i : ι), ∃ i', f i ≤ g i') → ⨆ i, f i ≤ ⨆ i', g i'
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_le_mul_of_nonneg'`. -/
mul_le_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α] [MulPosMono α],
  a ≤ b → c ≤ d → 0 ≤ c → 0 ≤ b → a * c ≤ b * d
-- Mathlib.CategoryTheory.Iso
/-- The inverse of a morphism `f` when we have `[IsIso f]`.  -/
CategoryTheory.inv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (f : X ⟶ Y) → [I : CategoryTheory.IsIso f] → Y ⟶ X