mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄}
  {f g :
    CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
        (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶
      A},
  f = g ↔
    ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) f =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) g
-- Mathlib.Geometry.Manifold.ChartedSpace
iUnion_source_chartAt : ∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M],
  ⋃ x, (chartAt H x).source = Set.univ
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.aemeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β}, MeasureTheory.MeasurePreserving f μa μb → AEMeasurable f μa
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The coordinates of a representative of `2 • P` for a Jacobian point representative `P` on a
Weierstrass curve.  -/
WeierstrassCurve.Jacobian.dblXYZ : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → Fin 3 → R
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.le_comap_of_map_le : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (S : L.Substructure M) {T : L.Substructure N} {f : L.Hom M N},
  FirstOrder.Language.Substructure.map f S ≤ T → S ≤ FirstOrder.Language.Substructure.comap f T
-- Mathlib.CategoryTheory.Limits.Creates
/-- Satisfy the inhabited linter  -/
CategoryTheory.inhabitedLiftsToLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.CreatesLimit K F] →
                  (c : CategoryTheory.Limits.Cone (K.comp F)) →
                    (t : CategoryTheory.Limits.IsLimit c) → Inhabited (CategoryTheory.LiftsToLimit K F c t)
-- Mathlib.Data.Multiset.Replicate
Multiset.rel_replicate_right : ∀ {α : Type u_1} {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ},
  Multiset.Rel r m (Multiset.replicate n a) ↔ m.card = n ∧ ∀ x ∈ m, r x a
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.instTopologicalSpace.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] (N : Subgroup G),
  QuotientGroup.instTopologicalSpace N = instTopologicalSpaceQuotient
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Localization.mulEquivOfQuotient_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f : S.LocalizationMap N} (x : Localization S),
  (Localization.mulEquivOfQuotient f) x = ((Localization.monoidOf S).lift ⋯) x
-- Init.System.Promise
_private.Init.System.Promise.0.IO.Option.getOrBlock! : {α : Type u_1} → [Nonempty α] → Option α → α
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracket_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E},
  VectorField.lieBracket 𝕜 V W = fun x => (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x)
-- Mathlib.Data.Multiset.MapFold
Multiset.eq_of_mem_map_const : ∀ {α : Type u_1} {β : Type v} {b₁ b₂ : β} {l : List α}, b₁ ∈ Multiset.map (Function.const α b₂) ↑l → b₁ = b₂
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.instSMulHom : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → SMul (CategoryTheory.CatCenter C) (X ⟶ Y)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {f : Option β → Option β},
  (t.alter k f).isEmpty = false →
    ((t.alter k f).minKey! = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_iInf : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {ι : Sort u_1} {S : ι → NonUnitalSubring R}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
/-- If `α` has at least 5 elements, but not 8,
then the only nontrivial normal subgroup of `alternatingGroup α`
is `⊤`.  -/
alternatingGroup.normal_subgroup_eq_bot_or_eq_top_of_card_ne_eight : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  5 ≤ Nat.card α → Nat.card α ≠ 8 → ∀ {N : Subgroup ↥(alternatingGroup α)} [N.Normal], N = ⊥ ∨ N = ⊤
-- Mathlib.RingTheory.LocalProperties.IntegrallyClosed
isIntegrallyClosed_ofLocalizationMaximal : OfLocalizationMaximal fun R x => ∀ [IsDomain R], IsIntegrallyClosed R
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id : ∀ {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.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive],
  CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.CategoryStruct.id F.leftDerivedToHomotopyCategory
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.eval_lt : ∀ {b e : Ordinal.{u_1}} {f : Ordinal.{u_1} →₀ Ordinal.{u_1}},
  (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → Ordinal.CNF.eval b f < b ^ e
-- Mathlib.Algebra.Order.Module.Defs
PosSMulStrictMono.toSMulPosStrictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : AddCommGroup β]
  [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulStrictMono α β], SMulPosStrictMono α β
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.pred'.match_1.eq_1 : ∀ (motive : PosNum → Sort u_1) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match PosNum.one with
    | PosNum.one => h_1 ()
    | n.bit0 => h_2 n
    | n.bit1 => h_3 n) =
    h_1 ()
-- Mathlib.Util.Export
_private.Mathlib.Util.Export.0.Lean.Export.exportDef.insert : Lean.Name → Lean.ExportM Unit
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.top_rpow_def : ∀ (y : ℝ), ⊤ ^ y = if 0 < y then ⊤ else if y = 0 then 1 else 0
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- If a family of sets `𝒜` is measure-dense in `X`, then any measurable set with finite measure
can be approximated by sets in `𝒜` with finite measure.  -/
MeasureTheory.Measure.MeasureDense.fin_meas_approx : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)},
  μ.MeasureDense 𝒜 →
    ∀ {s : Set X}, MeasurableSet s → μ s ≠ ⊤ → ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ t ≠ ⊤ ∧ μ (symmDiff s t) < ENNReal.ofReal ε
-- Mathlib.Algebra.Group.Equiv.TypeTags
monoidEndToAdditive_apply_apply : ∀ (M : Type u_4) [inst : MulOneClass M] (f : M →* M) (a : Additive M),
  ((monoidEndToAdditive M) f) a = Additive.ofMul (f (Additive.toMul a))
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsMaximumIndepSet.isIndepSet : ∀ {α : Type u_3} [inst : Finite α] {G : SimpleGraph α} {s : Finset α}, G.IsMaximumIndepSet s → G.IsIndepSet ↑s
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_exact : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' pq'' : κ),
  (c r).next pq' = pq'' →
    ∀ (i₀' i₀ i₁ i₂ i₃ : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq')
      (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
      [X.HasSpectralSequence data]
      (hn₁ :
        autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_exact._auto_1)
      (hn₂ :
        autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_exact._auto_3),
      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁
          i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).Exact
-- Mathlib.Algebra.Group.Semiconj.Units
AddSemiconjBy.addUnits_val_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {a x y : AddUnits M}, AddSemiconjBy ↑a ↑x ↑y ↔ AddSemiconjBy a x y
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- `Pi.orthonormalBasis (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i))` is the
`Σ i, ι i`-indexed orthonormal basis on `Π i, E i` given by `B i` on each component.  -/
Pi.orthonormalBasis : {η : Type u_7} →
  [inst : Fintype η] →
    {ι : η → Type u_8} →
      [inst_1 : (i : η) → Fintype (ι i)] →
        {𝕜 : Type u_9} →
          [inst_2 : RCLike 𝕜] →
            {E : η → Type u_10} →
              [inst_3 : (i : η) → NormedAddCommGroup (E i)] →
                [inst_4 : (i : η) → InnerProductSpace 𝕜 (E i)] →
                  ((i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) → OrthonormalBasis ((i : η) × ι i) 𝕜 (PiLp 2 E)
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.hasRightResolutions : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  [self : Φ.IsRightDerivabilityStructure], Φ.HasRightResolutions
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_mul_const' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a : E → 𝔸},
  DifferentiableAt 𝕜 a x → ∀ (b : 𝔸), fderiv 𝕜 (fun y => a y * b) x = MulOpposite.op b • fderiv 𝕜 a x
-- Std.Time.Date.PlainDate
/-- Returns the aligned week of the month for a `PlainDate`. Weeks are fixed 7-day slots
starting from day 1: days 1–7 are week 1, days 8–14 are week 2, etc.
 -/
Std.Time.PlainDate.alignedWeekOfMonth : Std.Time.PlainDate → Std.Time.Week.Aligned.Ordinal
-- Lean.Server.Requests
Lean.Server.RequestM.waitFindSnapAux : {α : Type} →
  Lean.Server.RequestM α →
    (Lean.Server.Snapshots.Snapshot → Lean.Server.RequestM α) →
      Except IO.Error (Option Lean.Server.Snapshots.Snapshot) → Lean.Server.RequestM α
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- Given a multilinear map `f` in `n+1` variables, split the first variable to obtain
a linear map into multilinear maps in `n` variables, given by `x ↦ (m ↦ f (cons x m))`.  -/
MultilinearMap.curryLeft : {R : Type uR} →
  {n : ℕ} →
    {M : Fin n.succ → Type v} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : Fin n.succ) → Module R (M i)] →
                [inst_4 : Module R M₂] → MultilinearMap R M M₂ → M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.ae_lt_top' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → ∀ᵐ (x : α) ∂μ, f x < ⊤
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.ge_one_le : ∀ {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]
  (self : CategoryTheory.Triangulated.TStructure C), self.ge 1 ≤ self.ge 0
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmoothOfRelativeDimension.mk : ∀ {n : ℕ} {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (∃ ι σ, ∃ (x : Finite σ) (_ : Finite ι), ∃ P, P.dimension = n) → Algebra.IsStandardSmoothOfRelativeDimension n R S
-- Init.Data.Vector.InsertIdx
Vector.insertIdx_size_self : ∀ {α : Type u} {n : ℕ} {xs : Vector α n} {x : α}, xs.insertIdx n x ⋯ = xs.push x
-- Mathlib.Algebra.Module.Torsion.Basic
Ideal.torsionOf_eq_top_iff : ∀ (R : Type u_1) {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M),
  Ideal.torsionOf R M m = ⊤ ↔ m = 0
-- Init.Data.Nat.Lemmas
Nat.mul_div_mul_comm : ∀ {a b c d : ℕ}, b ∣ a → d ∣ c → a * c / (b * d) = a / b * (c / d)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.decomp_from : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {j : ℤ} {A : C}
  (f : (CochainComplex.mappingCone φ).X j ⟶ A) (i : ℤ) (hij : j + 1 = i),
  ∃ a b,
    f =
      CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v j i hij) a +
        CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v j j ⋯) b
-- Mathlib.NumberTheory.Padics.Complex
PadicAlgCl.instUniformContinuousConstSMulPadic : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], UniformContinuousConstSMul ℚ_[p] (PadicAlgCl p)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.dpEqualizer_is_dp_ideal_right : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I), hI'.IsSubDPIdeal (hI.dpEqualizer hI')
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_erase_le_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k km kme : α} (hkme : (t.erase k).maxKey? = some kme), t.maxKey?.get ⋯ = km → (cmp kme km).isLE = true
-- Mathlib.Algebra.Order.Group.Cone
GroupConeClass.eq_one_of_mem_of_inv_mem : ∀ {S : Type u_1} {G : outParam (Type u_2)} {inst : CommGroup G} {inst_1 : SetLike S G} [self : GroupConeClass S G]
  {C : S} {a : G}, a ∈ C → a⁻¹ ∈ C → a = 1
-- Mathlib.Algebra.Notation.Support
Pi.mulSupport_mulSingle_subset : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : One M] {i : ι} {a : M},
  Function.mulSupport (Pi.mulSingle i a) ⊆ {i}
-- Mathlib.Tactic.SplitIfs
/-- Returns `true` if the condition or its negation already appears as a hypothesis.
 -/
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.valueKnown : Lean.Expr → Lean.Elab.Tactic.TacticM Bool
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.mem_saturation_iff_exists_dvd : ∀ {M : Type u_1} [inst : CommMonoid M] {s : Submonoid M} {x : M}, x ∈ s.saturation ↔ ∃ m ∈ s, x ∣ m
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.isMonoidal_comp : ∀ {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]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_6 : F.OplaxMonoidal]
  [inst_7 : G.LaxMonoidal] [adj.IsMonoidal] {F' : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor E D}
  (adj' : F' ⊣ G') [inst_9 : F'.OplaxMonoidal] [inst_10 : G'.LaxMonoidal] [adj'.IsMonoidal], (adj.comp adj').IsMonoidal
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.forM_eq_forMUncurried : ∀ {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Monad m] [LawfulMonad m] {f : α → β → m PUnit.{w + 1}},
  Std.DTreeMap.Raw.forM f t = Std.DTreeMap.Raw.Const.forMUncurried (fun a => f a.1 a.2) t
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.combineMinIdxOn_lt : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) {xs ys : List α} {i j : ℕ}
  (hi : i < xs.length) (hj : j < ys.length), List.combineMinIdxOn✝ f i j hi hj < (xs ++ ys).length
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.card_biUnion_le : ∀ {ι : Type u_1} {M : Type u_4} [inst : DecidableEq M] {s : Finset ι} {t : ι → Finset M},
  (s.biUnion t).card ≤ ∑ a ∈ s, (t a).card
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
Nat.Partition.coeff_genFun : ∀ {R : Type u_1} [inst : CommSemiring R] (f : ℕ → ℕ → R) (n : ℕ),
  (PowerSeries.coeff n) (Nat.Partition.genFun f) = ∑ p, (Multiset.toFinsupp p.parts).prod f
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_sliceFrom_eq_false_iff : ∀ {s : String} {p : s.Pos}, (s.sliceFrom p).isEmpty = false ↔ p ≠ s.endPos
-- Mathlib.RingTheory.Polynomial.SmallDegreeVieta
/-- **Vieta's formula** for quadratics (`aroots` version).  -/
Polynomial.eq_neg_mul_add_of_aroots_quadratic_eq_pair : ∀ {T : Type u_2} {S : Type u_3} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  {a b c : T} {x1 x2 : S},
  (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).aroots S = {x1, x2} →
    (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2)
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- **Alias** of `SemimoduleCat.hom_nsmul`. -/
SemimoduleCat.hom_zsmul : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} (n : ℕ) (f : M ⟶ N),
  SemimoduleCat.Hom.hom (n • f) = n • SemimoduleCat.Hom.hom f
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.ιChainComplex_d_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) {n : ℕ} (x : X.obj (Opposite.op { len := n + 1 })) {Z : C}
  (h : (X.chainComplex R).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιChainComplex x)
      (CategoryTheory.CategoryStruct.comp ((X.chainComplex R).d (n + 1) n) h) =
    CategoryTheory.CategoryStruct.comp
      (∑ x_1,
        (-1) ^ ↑x_1 •
          X.ιChainComplex ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X x_1)) x))
      h
-- Std.Data.HashMap.Lemmas
Std.HashMap.forM_eq_forM_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → m' PUnit.{w + 1}},
  Std.HashMap.forM (fun a x => f a) m = Array.forM f m.keysArray
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.smul_slash : ∀ (k : ℤ) (A : GL (Fin 2) ℝ) (f : UpperHalfPlane → ℂ) (c : ℂ),
  SlashAction.map k A (c • f) = (UpperHalfPlane.σ A) c • SlashAction.map k A f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
MeasureTheory.AEStronglyMeasurable.inner : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {m x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun x => inner 𝕜 (f x) (g x)) μ
-- Mathlib.LinearAlgebra.Multilinear.Basis
Basis.multilinearMap.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {M : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {κ : ι → Type u_5} (b : (i : ι) → Module.Basis (κ i) R (M i)) {ι' : Type u_6}
  {N : Type u_7} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (b' : Module.Basis ι' R N) [inst_5 : Finite ι]
  [inst_6 : ∀ (i : ι), Finite (κ i)],
  Basis.multilinearMap b b' =
    {
      repr :=
        have this := Fintype.ofFinite ι;
        have this_1 := fun i => Fintype.ofFinite (κ i);
        ((LinearEquiv.multilinearMapCongrLeft fun i => (b i).repr.symm).trans
              (LinearEquiv.multilinearMapCongrRight R b'.repr)).trans
          MultilinearMap.freeFinsuppEquiv.symm }
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.toTopologicalSpace_bot : ∀ {α : Type u} [inst : Group α], ⊥.toTopologicalSpace = ⊥
-- Batteries.Data.Fin.Lemmas
Fin.countP_one : ∀ (p : Fin 1 → Bool), Fin.countP p = (p 0).toNat
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarDecl : Type
-- Lean.Parser.Do
Lean.Parser.Term.dependentParam.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.Iterators.Lemmas.Combinators.Zip
/-- Constructs intermediate states of an iterator created with the combinator `Iter.zip`.
When `left.zip right` has already obtained a value from `left` but not yet from right,
it remembers `left`'s value in a field of its internal state. This intermediate state
cannot be created directly with `Iter.zip`.

`Intermediate.zip` is meant to be used only for verification purposes.
 -/
Std.Iter.Intermediate.zip : {α₁ α₂ β₁ β₂ : Type w} →
  [inst : Std.Iterator α₁ Id β₁] →
    Std.Iter β₁ → Option { out // ∃ it, it.toIterM.IsPlausibleOutput out } → Std.Iter β₂ → Std.Iter (β₁ × β₂)
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- Predicate for edge adjacency. Analogous to `Hypergraph.Adj`, edges `e` and `f` are
adjacent if there is some vertex `x ∈ V(H)` where `x` is incident to both `e` and `f`.
 -/
Hypergraph.EAdj : {α : Type u_1} → Hypergraph α → Set α → Set α → Prop
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqCases : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Cases pu → Lean.Compiler.LCNF.Cases pu → Bool
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.finsetSum_mem_finsetSum`.

---

An n-ary version of `Set.add_mem_add`.  -/
Set.finset_sum_mem_finset_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α),
  (∀ i ∈ t, g i ∈ f i) → ∑ i ∈ t, g i ∈ ∑ i ∈ t, f i
-- Mathlib.LinearAlgebra.Basis.Basic
/-- Given a basis, the `i`th element of the dual basis evaluates to the Kronecker delta on the
`j`th element of the basis.  -/
Module.Basis.mk_coord_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} {hli : LinearIndependent R v} {hsp : ⊤ ≤ Submodule.span R (Set.range v)} [inst_3 : DecidableEq ι]
  {i j : ι}, ((Module.Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0