mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNorm_sub_le_of_dist_bdd : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {s : Set α} {β : Type u_9} [inst : NormedAddCommGroup β]
  (μ : autoParam (MeasureTheory.Measure α) MeasureTheory.eLpNorm_sub_le_of_dist_bdd._auto_1),
  p ≠ ⊤ →
    MeasurableSet s →
      ∀ {c : ℝ},
        0 ≤ c →
          ∀ {f g : α → β},
            (∀ (x : α), dist (f x) (g x) ≤ c) →
              Function.support f ⊆ s →
                Function.support g ⊆ s → MeasureTheory.eLpNorm (f - g) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.val_step_takeWhile.match_3.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Probability.Moments.Basic
ContinuousLinearMap.integral_comp_id_comm' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] [inst_9 : MeasurableSpace E]
  {μ : MeasureTheory.Measure E},
  MeasureTheory.Integrable id μ → ∀ (L : E →L[𝕜] F), ∫ (x : E), L x ∂μ = L (∫ (x : E), id x ∂μ)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.singleAddHom_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] (a : G) (b : k),
  (SkewMonoidAlgebra.singleAddHom a) b = SkewMonoidAlgebra.single a b
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂'_add_left' : ∀ (z τ : ℂ),
  jacobiTheta₂' (z + τ) τ =
    Complex.exp (-↑Real.pi * Complex.I * (τ + 2 * z)) *
      (jacobiTheta₂' z τ - 2 * ↑Real.pi * Complex.I * jacobiTheta₂ z τ)
-- Mathlib.Algebra.Group.Equiv.Opposite
MulOpposite.coe_opMulEquiv : ∀ {M : Type u_1} [inst : CommMonoid M], ⇑MulOpposite.opMulEquiv = MulOpposite.op
-- Mathlib.Analysis.Normed.Group.InfiniteSum
hasSum_iff_tendsto_nat_of_summable_norm : ∀ {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ℕ → E} {a : E},
  (Summable fun i => ‖f i‖) → (HasSum f a ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds a))
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.packedNaN.eq_1 : ∀ (spec : Float.Model.Format),
  Float.Model.UnpackedFloat.packedNaN spec =
    Float.Model.UnpackedFloat.packComponents spec Float.Model.UnpackedFloat.Sign.positive (-1#spec.exponentBits)
      (1#spec.mantissaBitsWithoutImplicit <<< (spec.mantissaBitsWithoutImplicit - 1))
-- Mathlib.Data.Set.Basic
Set.subset_ofPred : ∀ {α : Type u} {p : α → Prop} {s : Set α}, s ⊆ Set.ofPred p ↔ ∀ x ∈ s, p x
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.constVSub_symm_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] (p : P₁) (x : V₁), (ContinuousAffineEquiv.constVSub k p).symm x = -x +ᵥ p
-- Mathlib.NumberTheory.Padics.MahlerBasis
ZeroAtInftyContinuousMap.mk.congr_simp : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (toContinuousMap toContinuousMap_1 : C(α, β)) (e_toContinuousMap : toContinuousMap = toContinuousMap_1)
  (zero_at_infty' : Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (nhds 0)),
  { toContinuousMap := toContinuousMap, zero_at_infty' := zero_at_infty' } =
    { toContinuousMap := toContinuousMap_1, zero_at_infty' := ⋯ }
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_le_indicator_of_subset : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : Zero M] {s t : Set α} {f : α → M},
  s ⊆ t → 0 ≤ f → s.indicator f ≤ t.indicator f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.Internal.List.maxKey?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (xs : List ((a : α) × β a)),
  Std.Internal.List.maxKey? xs = Std.Internal.List.minKey? xs
-- Mathlib.Computability.Language
Language.iSup_add : ∀ {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α), (⨆ i, l i) + m = ⨆ i, l i + m
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.beq.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Batteries.AssocList α β → Batteries.AssocList α β → Sort u_3)
  (h_1 : Unit → motive Batteries.AssocList.nil Batteries.AssocList.nil)
  (h_2 :
    (key : α) →
      (value : β) →
        (tail : Batteries.AssocList α β) → motive (Batteries.AssocList.cons key value tail) Batteries.AssocList.nil)
  (h_3 :
    (key : α) →
      (value : β) →
        (tail : Batteries.AssocList α β) → motive Batteries.AssocList.nil (Batteries.AssocList.cons key value tail))
  (h_4 :
    (a : α) →
      (b : β) →
        (t : Batteries.AssocList α β) →
          (a' : α) →
            (b' : β) →
              (t' : Batteries.AssocList α β) →
                motive (Batteries.AssocList.cons a b t) (Batteries.AssocList.cons a' b' t')),
  (match Batteries.AssocList.nil, Batteries.AssocList.nil with
    | Batteries.AssocList.nil, Batteries.AssocList.nil => h_1 ()
    | Batteries.AssocList.cons key value tail, Batteries.AssocList.nil => h_2 key value tail
    | Batteries.AssocList.nil, Batteries.AssocList.cons key value tail => h_3 key value tail
    | Batteries.AssocList.cons a b t, Batteries.AssocList.cons a' b' t' => h_4 a b t a' b' t') =
    h_1 ()
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.BVVar.mk.injEq : ∀ {width : ℕ} (ident ident_1 : ℕ), ({ ident := ident } = { ident := ident_1 }) = (ident = ident_1)
-- Mathlib.Control.Monad.Cont
ExceptT.callCC : {m : Type u → Type v} →
  [Monad m] →
    {ε : Type u} → [MonadCont m] → {α β : Type u} → (MonadCont.Label α (ExceptT ε m) β → ExceptT ε m α) → ExceptT ε m α
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.pi_symm_apply : ∀ {ι : Type u_7} [inst : Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [inst_1 : (i : ι) → TopologicalSpace (X i)]
  [inst_2 : (i : ι) → TopologicalSpace (Y i)] (ei : (i : ι) → OpenPartialHomeomorph (X i) (Y i)) (a : (i : ι) → Y i)
  (i : ι), ↑(OpenPartialHomeomorph.pi ei).symm a i = ↑(ei i).symm (a i)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C],
  (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ
-- Batteries.Data.List.Lemmas
List.findIdxsValues.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (start : ℕ),
  List.findIdxsValues p l start = List.foldrIdx (fun i a l => if p a = true then (i, a) :: l else l) [] l start
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.ofAdd_eq_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α] {a : α}, Multiplicative.ofAdd a = ⊤ ↔ a = ⊤
-- Init.GetElem
getElem?_eq_some_iff : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} {e : elem}
  [inst : GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)],
  c[i]? = some e ↔ ∃ (h : dom c i), c[i] = e
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_inter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.Const.get? (m₁.inter m₂ ⋯) k =
        if Std.DTreeMap.Internal.Impl.contains k m₂ = true then Std.DTreeMap.Internal.Impl.Const.get? m₁ k else none
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If `C` is cofiltered or empty, and we have a left adjoint functor `L : C ⥤ D`, then `D` is
cofiltered or empty.  -/
CategoryTheory.IsCofilteredOrEmpty.of_isLeftAdjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (L : CategoryTheory.Functor C D) [L.IsLeftAdjoint],
  CategoryTheory.IsCofilteredOrEmpty D
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionClientCapabilities : Lean.FromJson Lean.Lsp.CodeActionClientCapabilities
-- Lean.Message
Lean.MessageData.originatingSyntax? : Lean.MessageData → Option Lean.Syntax × Lean.MessageData
-- Mathlib.SetTheory.ZFC.PSet
/-- Insert an element into a pre-set  -/
PSet.insert : PSet.{u_1} → PSet.{u_1} → PSet.{u_1}
-- Lean.Elab.PreDefinition.WF.Fix
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.replaceRecApps.loopGo : (recFnName : Lean.Name) → ℕ → Lean.Expr → Lean.Expr → Lean.Elab.WF.RecM✝ recFnName Lean.Expr
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_iExs : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {γ : Type u_3} [inst_1 : Finite γ]
  {φ : L.Formula (α ⊕ γ)} {v : α → M} {v' : Fin 0 → M},
  FirstOrder.Language.BoundedFormula.Realize (FirstOrder.Language.Formula.iExs γ φ) v v' ↔ ∃ i, φ.Realize (Sum.elim v i)
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousWithinAt.congr_of_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → Set β} {s : Set α}
  {a : α},
  UpperHemicontinuousWithinAt f s a →
    a ∈ s → (∀ᶠ (x : α) in nhdsWithin a s, f x = g x) → UpperHemicontinuousWithinAt g s a
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.single_toFun : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] {ι : Type u_7}
  [inst_2 : DecidableEq ι] (i : ι) (x : HahnSeries Γ R) (j : ι),
  (HahnSeries.SummableFamily.single i x) j = Pi.single i x j
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termL₂ : Lean.ParserDescr
-- Mathlib.Data.ZMod.Basic
/-- This cannot be made an instance because of the `[Module (ZMod n) G]` argument and the fact that
`n` only appears in the second argument of `SMulMemClass`, which is an `OutParam`.  -/
smulMemClass : ∀ {n : ℕ} {S : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : SetLike S G] [AddSubgroupClass S G]
  [inst_3 : Module (ZMod n) G], SMulMemClass S (ZMod n) G
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_apply_prime : ∀ {p : ℕ}, Nat.Prime p → ArithmeticFunction.cardFactors p = 1
-- Mathlib.Algebra.Module.LinearMap.End
RingEquiv.moduleEndSelfOp_symm_apply : ∀ (R : Type u_1) [inst : Semiring R] (f : Module.End Rᵐᵒᵖ R), (RingEquiv.moduleEndSelfOp R).symm f = f 1
-- Mathlib.Analysis.LocallyConvex.AbsConvex
/-- A set is absolutely convex if it is balanced and convex.  -/
AbsConvex : (𝕜 : Type u_1) → {E : Type u_2} → [SeminormedRing 𝕜] → [SMul 𝕜 E] → [AddCommMonoid E] → [PartialOrder 𝕜] → Set E → Prop
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.card_pair_lcm_eq.f : {n : ℕ} → (a : Fin 3 → ℕ) → a ∈ Nat.finMulAntidiag 3 n → ℕ × ℕ
-- Mathlib.Algebra.Notation.Prod
Prod.instMul : {M : Type u_8} → {N : Type u_9} → [Mul M] → [Mul N] → Mul (M × N)
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.toPoly : Nat.Internal.SOM.Expr → Nat.Internal.SOM.Poly
-- Std.Internal.Do.WP.Conjunctive
_private.Std.Internal.Do.WP.Conjunctive.0.Std.Internal.Do.EStateM.wpInst.match_1.eq_1 : ∀ {ε σ α : Type} (motive : EStateM.Result ε σ α → Sort u_1) (a : α) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (el : ε) → (s' : σ) → motive (EStateM.Result.error el s')),
  (match EStateM.Result.ok a s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error el s' => h_2 el s') =
    h_1 a s'
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.packingNumber_zero : ∀ {E : Type u_3} [inst : EMetricSpace E] (A : Set E), Metric.packingNumber 0 A = A.encard
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
  IsUpperSet s → ∀ {f : β → α}, Monotone f → IsUpperSet (f ⁻¹' s)
-- Mathlib.AlgebraicGeometry.SpreadingOut
/-- The class of schemes such that for each `x : X`,
`Γ(X, U) ⟶ X_x` is injective for some affine `U` containing `x`.

This is typically satisfied when `X` is integral or locally Noetherian.
 -/
AlgebraicGeometry.Scheme.IsGermInjective : AlgebraicGeometry.Scheme → Prop
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.dist_mulExpNegMulSq_le_dist : ∀ {ε : ℝ}, 0 < ε → ∀ {x y : ℝ}, dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.containsKey_filter_iff : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {f : α → β → Bool} {l : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.containsKey k (List.filter (fun p => f p.fst p.snd) l) = true ↔
      ∃ (h : Std.Internal.List.containsKey k l = true),
        f (Std.Internal.List.getKey k l h) (Std.Internal.List.getValue k l h) = true)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.comp_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y Z : SheafOfModules R} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_apply_of_aleph0_le : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → Cardinal.toNat c = 0
-- Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Algebra.FinitePresentation.pi : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_3} [Finite ι] (S : ι → Type u_4) [inst_2 : (i : ι) → CommRing (S i)]
  [inst_3 : (i : ι) → Algebra R (S i)] [∀ (i : ι), Algebra.FinitePresentation R (S i)],
  Algebra.FinitePresentation R ((a : ι) → S a)
-- Mathlib.Algebra.MvPolynomial.Equiv
_private.Mathlib.Algebra.MvPolynomial.Equiv.0.Option.elim.match_1.eq_1 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (x : α) (x_1 : β) (f : α → β)
  (h_1 : (x : α) → (x_2 : β) → (f : α → β) → motive (some x) x_2 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match some x, x_1, f with
    | some x, x_2, f => h_1 x x_2 f
    | none, y, x => h_2 y x) =
    h_1 x x_1 f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.const_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {𝕜 : Type u_5} [inst_1 : SMul 𝕜 β] [ContinuousConstSMul 𝕜 β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : 𝕜), MeasureTheory.AEStronglyMeasurable (c • f) μ
-- Mathlib.Order.Category.FinBddDistLat
/-- Constructs an equivalence between finite distributive lattices from an order isomorphism
between them.  -/
FinBddDistLat.Iso.mk : {α β : FinBddDistLat} → ↑α.toDistLat ≃o ↑β.toDistLat → (α ≅ β)
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- The colimit of `coyoneda.obj X` is isomorphic to `PUnit`.
 -/
CategoryTheory.Coyoneda.colimitCoyonedaIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : Cᵒᵖ) → CategoryTheory.Limits.colimit (CategoryTheory.coyoneda.obj X) ≅ PUnit.{v + 1}
-- Mathlib.GroupTheory.DivisibleHull
_private.Mathlib.GroupTheory.DivisibleHull.0.DivisibleHull.lift_aux : ∀ {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [IsOrderedCancelAddMonoid M] (m n m' n' : M)
  (s t s' t' : ℕ+),
  DivisibleHull.mk m s = DivisibleHull.mk m' s' →
    DivisibleHull.mk n t = DivisibleHull.mk n' t' → (↑t • m ≤ ↑s • n) = (↑t' • m' ≤ ↑s' • n')
-- Mathlib.Data.Fin.SuccPred
/-- `castSucc` commutes with `succAbove`.  -/
Fin.castSucc_succAbove_castSucc : ∀ {n : ℕ} {i : Fin (n + 1)} {j : Fin n}, i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
-- Mathlib.Algebra.Group.Hom.Instances
instIsCancelAddAddMonoidHom : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] [IsCancelAdd N], IsCancelAdd (M →+ N)
-- Mathlib.Util.Notation3
/-- Matcher for processing `scoped` syntax. Assumes the expression to be matched
against is in the `lit` variable.

Runs `smatcher`, extracts the resulting `scopeId` variable, processes this value
(which must be a lambda) to produce a binder, and loops.  -/
Mathlib.Notation3.matchScoped : Lean.Name → Lean.Name → Mathlib.Notation3.Matcher → Mathlib.Notation3.Matcher
-- Lean.KeyedDeclsAttribute
/-- `KeyedDeclsAttribute` definition.

Important: `mkConst valueTypeName` and `γ` must be definitionally equal.  -/
Lean.KeyedDeclsAttribute.Def : Type → Type
-- Mathlib.Algebra.Group.Submonoid.Support
/-- A submonoid `M` of a group `G` is spanning if `M` generates `G` as a subgroup.  -/
AddSubmonoid.IsSpanning : {G : Type u_1} → [inst : AddGroup G] → AddSubmonoid G → Prop
-- Init.Data.Array.Lemmas
Array.flatMap_def : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β}, Array.flatMap f xs = (Array.map f xs).flatten
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality : ∀ {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] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X)
  (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0) →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ),
      CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).inv ((F.rightDerived n).map f) =
        CategoryTheory.CategoryStruct.comp
          (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp
                (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map
            φ)
          (J.isoRightDerivedObj F n).inv
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearMap.comap_eq_sup_ker_of_disjoint : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {p : Submodule K V}
  [FiniteDimensional K ↥p] {f : V →ₗ[K] V}, (∀ x ∈ p, f x ∈ p) → Disjoint p f.ker → Submodule.comap f p = p ⊔ f.ker
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.add_lt_eq : ∀ {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α],
  a₁ < b₁ → a₂ = b₂ → a₁ + a₂ < b₁ + b₂
-- Mathlib.CategoryTheory.Sites.Finite
CategoryTheory.Precoverage.ofArrows_mem_finite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {ι : Type u_1} [Finite ι] (Y : ι → C)
  (f : (i : ι) → Y i ⟶ X), CategoryTheory.Presieve.ofArrows Y f ∈ (CategoryTheory.Precoverage.finite C).coverings X
-- Init.Data.BitVec.Bitblast
BitVec.DivModState.Poised.toLawful : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Poised args qr → BitVec.DivModState.Lawful args qr
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOn.add` -/
TendstoUniformlyOn.fun_add : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β},
  TendstoUniformlyOn f g l s →
    TendstoUniformlyOn f' g' l s → TendstoUniformlyOn (fun i i_1 => f i i_1 + f' i i_1) (fun i => g i + g' i) l s
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SavedState.meta : Lean.Meta.Grind.SavedState → Lean.Meta.SavedState
-- Init.Data.List.MinMaxIdx
List.ne_nil_of_minIdxOn?_eq_some : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {k : ℕ} {xs : List α},
  List.minIdxOn? f xs = some k → xs ≠ []
-- Mathlib.Condensed.Light.Functors
/-- `lightProfiniteToLightCondSet` is fully faithful.  -/
lightProfiniteToLightCondSetFullyFaithful : lightProfiniteToLightCondSet.FullyFaithful
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodProdProdComm_symm : ∀ (M : Type u_3) (N : Type u_4) [inst : MulOneClass M] [inst_1 : MulOneClass N] (M' : Type u_6) (N' : Type u_7)
  [inst_2 : MulOneClass N'] [inst_3 : MulOneClass M'],
  (MulEquiv.prodProdProdComm M N M' N').symm = MulEquiv.prodProdProdComm M M' N N'
-- Std.Data.DHashMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.DHashMap.modify : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → Std.DHashMap α β → (a : α) → (β a → β a) → Std.DHashMap α β
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_succ_right : ∀ (R : Type u) [inst : Ring R] (n : ℕ), descPochhammer R (n + 1) = descPochhammer R n * (Polynomial.X - ↑n)
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.squareCylinders.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} (C : (i : ι) → Set (Set (α i))),
  MeasureTheory.squareCylinders C = {S | ∃ s, ∃ t ∈ Set.univ.pi C, S = (↑s).pi t}
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.map.eq_def : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f : (a : α) → β a → γ a)
  (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.map f t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner sz k v l r =>
      Std.DTreeMap.Internal.Impl.inner sz k (f k v) (Std.DTreeMap.Internal.Impl.map f l)
        (Std.DTreeMap.Internal.Impl.map f r)
-- Lean.Parser.Term
Lean.Parser.Term.fromTerm.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {k : α} {f : β k → β k} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.minKey? (Std.Internal.List.modifyKey k f l) = Std.Internal.List.minKey? l
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.blocksFun_pos : ∀ {n : ℕ} (c : CompositionAsSet n) (i : Fin c.length), 0 < c.blocksFun i
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α} {k : α} {h : k ∈ Std.HashMap.unitOfList l},
  (Std.HashMap.unitOfList l)[k] = ()
-- Init.Data.Rat.Basic
Rat.instMax : Max ℚ
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_eq_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [LawfulBEq α] [inst_2 : Inhabited α] {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k l = true → Std.Internal.List.getKey! k l = k
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.PreIndSpreads.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  (∀ {J : Type w} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J]
      {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D} (x : CategoryTheory.Limits.IsColimit c)
      {T : C} (f : c.pt ⟶ T), P f → ∃ j T' f' g, CategoryTheory.IsPushout (c.ι.app j) f' f g ∧ P f') →
    P.PreIndSpreads