mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Basic
/-- Returns a list of all keys present in the tree map in ascending  order.  -/
Std.DTreeMap.keys : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → List α
-- Mathlib.Algebra.Group.ULift
ULift.divInvMonoid.eq_1 : ∀ {α : Type u} [inst : DivInvMonoid α], ULift.divInvMonoid = Function.Injective.divInvMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.mapAlong_continuous : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) [inst : (i : ι₁) → TopologicalSpace (R₁ i)]
  [inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)}
  {A₂ : (i : ι₂) → Set (R₂ i)} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) (φ : (j : ι₂) → R₁ (f j) → R₂ j)
  (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo (φ j) (A₁ (f j)) (A₂ j)),
  (∀ (j : ι₂), Continuous (φ j)) → Continuous (RestrictedProduct.mapAlong R₁ R₂ f hf φ hφ)
-- Init.Data.SInt.Basic
/-- Bitwise left shift for 8-bit signed integers. Usually accessed via the `<<<` operator.

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.shiftLeft : Int8 → Int8 → Int8
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f g : α → E},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → μ.withDensityᵥ (f + g) = μ.withDensityᵥ f + μ.withDensityᵥ g
-- Mathlib.Data.Set.Finite.Basic
/-- If a function `f` has a partial inverse `g` and the image of `s` under `f` is a set with
a `Fintype` instance, then `s` has a `Fintype` structure as well.  -/
Set.fintypeOfFintypeImage : {α : Type u} →
  {β : Type v} →
    (s : Set α) → {f : α → β} → {g : β → Option α} → Function.IsPartialInv f g → [Fintype ↑(f '' s)] → Fintype ↑s
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
_private.Mathlib.Geometry.Manifold.VectorField.LieBracket.0.VectorField.mpullbackWithin_mlieBracketWithin_aux : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [IsManifold I 2 M]
  [inst_12 : IsManifold I' 2 M'] [CompleteSpace E] [CompleteSpace E'] {f : M → M'} {V W : (x : M') → TangentSpace I' x}
  {x₀ : M} {s : Set M} {t : Set M'},
  MDiffAt[t] (T% V) (f x₀) →
    MDiffAt[t] (T% W) (f x₀) →
      UniqueMDiff[s] →
        ContMDiffOn I I' 2 f s →
          x₀ ∈ s →
            t ⊆ (extChartAt I' (f x₀)).source →
              Set.MapsTo f s t →
                IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
                    (↑(extChartAt I x₀).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x₀) x₀) →
                  VectorField.mpullbackWithin I I' f (VectorField.mlieBracketWithin I' V W t) s x₀ =
                    VectorField.mlieBracketWithin I (VectorField.mpullbackWithin I I' f V s)
                      (VectorField.mpullbackWithin I I' f W s) s x₀
-- Aesop.RuleSet
Aesop.LocalRuleSet.mk.sizeOf_spec : ∀ (toBaseRuleSet : Aesop.BaseRuleSet) (simpTheoremsArray : Array (Lean.Name × Lean.Meta.SimpTheorems))
  (simpTheoremsArrayNonempty : 0 < simpTheoremsArray.size) (simprocsArray : Array (Lean.Name × Lean.Meta.Simprocs))
  (simprocsArrayNonempty : 0 < simprocsArray.size) (localNormSimpRules : Array Aesop.LocalNormSimpRule),
  sizeOf
      { toBaseRuleSet := toBaseRuleSet, simpTheoremsArray := simpTheoremsArray,
        simpTheoremsArrayNonempty := simpTheoremsArrayNonempty, simprocsArray := simprocsArray,
        simprocsArrayNonempty := simprocsArrayNonempty, localNormSimpRules := localNormSimpRules } =
    1 + sizeOf toBaseRuleSet + sizeOf simpTheoremsArray + sizeOf simpTheoremsArrayNonempty + sizeOf simprocsArray +
        sizeOf simprocsArrayNonempty +
      sizeOf localNormSimpRules
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  (ι : Type u_1) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S)
  {X_1 Y : (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra} (φ : X_1 ⟶ Y) (i : ι),
  ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).inverse.map φ).hom i = φ.f
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.range_fromSpecResidueField : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X), Set.range ⇑(X.fromSpecResidueField x) = {x}
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.coeff_mapDomainRingEquiv`. -/
MonoidAlgebra.mapDomainRingEquiv_apply : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (e : M ≃* N)
  (x : MonoidAlgebra R M), ((MonoidAlgebra.mapDomainRingEquiv R e) x).coeff = Finsupp.equivMapDomain (↑e) x.coeff
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_erase_eq_of_not_compare_minKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k fallback : α},
      (t.erase k).isEmpty = false →
        ¬cmp k (t.minKeyD fallback) = Ordering.eq → (t.erase k).minKeyD fallback = t.minKeyD fallback
-- Mathlib.Order.Filter.Germ.Basic
/-- Coercion `(α → R) → Germ l R` as a `RingHom`.  -/
Filter.Germ.coeRingHom : {α : Type u_1} → {R : Type u_5} → [inst : Semiring R] → (l : Filter α) → (α → R) →+* l.Germ R
-- Mathlib.NumberTheory.LSeries.Deriv
/-- The (point-wise) product of `log : ℕ → ℂ` with `f`.  -/
LSeries.logMul : (ℕ → ℂ) → ℕ → ℂ
-- Init.Data.Int.Order
Int.le_of_not_le : ∀ {a b : ℤ}, ¬a ≤ b → b ≤ a
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_inter_smul_inv : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  (A ∩ x • B⁻¹).card = A.convolution B x
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- If `α` is equipped with the lower set topology, then it is homeomorphic to `WithLowerSet α`.  -/
Topology.IsLowerSet.WithLowerSetHomeomorph : {α : Type u_1} →
  [inst : Preorder α] → [inst_1 : TopologicalSpace α] → [Topology.IsLowerSet α] → Topology.WithLowerSet α ≃ₜ α
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- If `f : ℝ → ℝ` is integrable on `(a, b]` for real numbers `a < b`, and positive on the interior
of the interval, then its integral over `a..b` is strictly positive.  -/
intervalIntegral.intervalIntegral_pos_of_pos_on : ∀ {f : ℝ → ℝ} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b → (∀ x ∈ Set.Ioo a b, 0 < f x) → a < b → 0 < ∫ (x : ℝ) in a..b, f x
-- Std.Sync.StreamMap
Std.instCoeDepAnyAsyncStreamOfAsyncStream : {t α : Type} → {x : t} → [Std.Async.IO.AsyncStream t α] → CoeDep t x (Std.AnyAsyncStream α)
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.setFind? : (self : ShareCommon.StateFactoryImpl) → self.Set → ShareCommon.Object → Option ShareCommon.Object
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonAssocSemiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M],
  AddMonoidAlgebra.nonAssocSemiring =
    { toNonUnitalNonAssocSemiring := AddMonoidAlgebra.nonUnitalNonAssocSemiring, toOne := AddMonoidAlgebra.zero,
      one_mul := ⋯, mul_one := ⋯, natCast := fun n => AddMonoidAlgebra.single 0 ↑n, natCast_zero := ⋯,
      natCast_succ := ⋯ }
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycleOn_swap : ∀ {α : Type u_2} {a b : α} [inst : DecidableEq α], a ≠ b → (Equiv.swap a b).IsCycleOn {a, b}
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.mono_L₀_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) [CategoryTheory.Mono S.L₁.f], CategoryTheory.Mono S.L₀.f
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_eq_monoidOf_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M}, Localization.mk = (Localization.monoidOf S).mk'
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.instIsAlgebraicSubtypeMemTop : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L], Algebra.IsAlgebraic (↥⊤) L
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.natDegree_natCast_le : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (↑n).natDegree ≤ 0
-- Mathlib.Topology.Specialization
Specialization.map_id : ∀ {α : Type u_1} [inst : TopologicalSpace α], Specialization.map (ContinuousMap.id α) = OrderHom.id
-- Mathlib.LinearAlgebra.Matrix.Symmetric
/-- A block matrix `A.fromBlocks B C D` is symmetric,
if `A` and `D` are symmetric and `Bᵀ = C`.  -/
Matrix.IsSymm.fromBlocks : ∀ {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
  {D : Matrix n n α}, A.IsSymm → B.transpose = C → D.IsSymm → (Matrix.fromBlocks A B C D).IsSymm
-- Lean.Server.References
/-- `ContextInfo` at the point of elaboration of this reference.  -/
Lean.Server.Reference.ci : Lean.Server.Reference → Lean.Elab.ContextInfo
-- Mathlib.Util.PPOptions
/-- The `pp.mathlib.binderPredicates` option is used to control whether mathlib pretty printers
should use binder predicate notation (such as `∀ x < 2, p x`).
 -/
Mathlib.pp.mathlib.binderPredicates : Lean.Option Bool
-- Mathlib.Data.Set.Lattice
Set.iUnion_comm : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (s : ι → ι' → Set α), ⋃ i, ⋃ i', s i i' = ⋃ i', ⋃ i, s i i'
-- Mathlib.CategoryTheory.Limits.EpiMono
CategoryTheory.mono_iff_isIso_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y}
  {c : CategoryTheory.Limits.PullbackCone f f} (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.fst
-- Mathlib.Algebra.Ring.Units
Units.val_eq_neg_one : ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] {a : αˣ}, ↑a = -1 ↔ a = -1
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueProds.instForall : ∀ {ι : Type u_2} (G : ι → Type u_1) [inst : (i : ι) → Mul (G i)] [∀ (i : ι), TwoUniqueProds (G i)],
  TwoUniqueProds ((i : ι) → G i)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k : α}, m.WF → k ∈ Std.HashMap.Raw.filterMap f m → k ∈ m
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.toAddGroupNorm : {R : Type u_2} → [inst : NonAssocRing R] → MulRingNorm R → AddGroupNorm R
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.congr_simp : ∀ {C : Type u₁} (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₂} D] (_F _F_1 : C → D),
  _F = _F_1 →
    ∀ (_P _P_1 : CategoryTheory.MorphismProperty D) (e__P : _P = _P_1) [inst_1 : _P.IsMultiplicative],
      CategoryTheory.InducedWideCategory D _F _P = CategoryTheory.InducedWideCategory D _F_1 _P_1
-- Mathlib.RingTheory.Invariant.Profinite
/-- `G` acts transitively on the prime ideals of `B` above a given prime ideal of `A`.  -/
Algebra.IsInvariant.exists_smul_of_under_eq_of_profinite : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {G : Type u}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [SMulCommClass G A B] [inst_6 : TopologicalSpace G]
  [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [inst_10 : TopologicalSpace B]
  [DiscreteTopology B] [ContinuousSMul G B] [Algebra.IsInvariant A B G] (P Q : Ideal B) [P.IsPrime] [Q.IsPrime],
  Ideal.under A P = Ideal.under A Q → ∃ g, Q = g • P
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.mk.inj : ∀ {R : Type u} {S : Type v} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S} {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} {inst_3 : CommRing R'} {inst_4 : CommRing S'} {inst_5 : Algebra R' S'}
  {P' : Algebra.Extension R' S'} {inst_6 : Algebra R R'} {inst_7 : Algebra S S'} {toRingHom : P.Ring →+* P'.Ring}
  {toRingHom_algebraMap :
    ∀ (x : R), toRingHom ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x)}
  {algebraMap_toRingHom :
    ∀ (x : P.Ring), (algebraMap P'.Ring S') (toRingHom x) = (algebraMap S S') ((algebraMap P.Ring S) x)}
  {toRingHom_1 : P.Ring →+* P'.Ring}
  {toRingHom_algebraMap_1 :
    ∀ (x : R), toRingHom_1 ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x)}
  {algebraMap_toRingHom_1 :
    ∀ (x : P.Ring), (algebraMap P'.Ring S') (toRingHom_1 x) = (algebraMap S S') ((algebraMap P.Ring S) x)},
  { toRingHom := toRingHom, toRingHom_algebraMap := toRingHom_algebraMap,
        algebraMap_toRingHom := algebraMap_toRingHom } =
      { toRingHom := toRingHom_1, toRingHom_algebraMap := toRingHom_algebraMap_1,
        algebraMap_toRingHom := algebraMap_toRingHom_1 } →
    toRingHom = toRingHom_1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β}, (m.insert k v)[a]? = if (k == a) = true then some v else m[a]?
-- Mathlib.RingTheory.Perfection
Perfection.coeff_mk : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] (f : ℕ → R)
  (hf : ∀ (n : ℕ), f (n + 1) ^ p = f n) (n : ℕ), (Perfection.coeff R p n) ⟨f, hf⟩ = f n
-- Mathlib.Logic.Function.Conjugate
/-- **Alias** of the forward direction of `Function.semiconj_iff_comp_eq`.

---

Definition of `Function.Semiconj` in terms of functional equality.  -/
Function.Semiconj.comp_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β}, Function.Semiconj f ga gb → f ∘ ga = gb ∘ f
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit.eq_def : ∀ (e : Lean.Expr) (omitTopForall : Bool),
  Lean.Elab.Command.NameGen.mkBaseNameCore.visit✝ e omitTopForall = do
    let __do_lift ← get
    if Std.HashSet.contains (Lean.Elab.Command.NameGen.MkNameState.seen✝ __do_lift) e = true then pure ""
      else do
        let s ← Lean.Elab.Command.NameGen.mkBaseNameCore.visit'✝ e omitTopForall
        modify fun st =>
            { seen := Std.HashSet.insert (Lean.Elab.Command.NameGen.MkNameState.seen✝ st) e,
              consts := Lean.Elab.Command.NameGen.MkNameState.consts✝ st }
        pure s
-- Mathlib.ModelTheory.Definability
Set.Definable.image_comp_equiv : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1}
  {s : Set (β → M)}, A.Definable L s → ∀ (f : α ≃ β), A.Definable L ((fun g => g ∘ ⇑f) '' s)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {v : β},
  (k, v) ∈ Std.ExtDTreeMap.Const.toList t ↔ Std.ExtDTreeMap.Const.get? t k = some v
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.of_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : SeminormedAddCommGroup β]
  {T : Set α → β} {C C' : ℝ},
  MeasureTheory.DominatedFinMeasAdditive μ T C → C ≤ C' → MeasureTheory.DominatedFinMeasAdditive μ T C'
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- A binary product of proper spaces is proper.  -/
prod_properSpace : ∀ {α : Type u_3} {β : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [ProperSpace α]
  [ProperSpace β], ProperSpace (α × β)
-- Lean.Meta.Tactic.SolveByElim
/-- If `symm` is `true`, then adds in symmetric versions of each hypothesis.
 -/
Lean.Meta.SolveByElim.saturateSymm : Bool → List Lean.Expr → Lean.MetaM (List Lean.Expr)
-- Mathlib.Order.Category.Preord
Preord.ofHom_id : ∀ {X : Type u} [inst : Preorder X],
  Preord.ofHom OrderHom.id = CategoryTheory.CategoryStruct.id { carrier := X, str := inst }
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_mk : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {s : Set M} {x : M} {h₁ : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ s → c • x ∈ s}
  {h₂ : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → x + y ∈ s}, x ∈ { carrier := s, smul_mem' := h₁, add_mem' := h₂ } ↔ x ∈ s
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.FunBinders.elabFunBinderViews : Array Lean.Elab.Term.BinderView →
  ℕ → Lean.Elab.Term.FunBinders.State → Lean.Elab.TermElabM Lean.Elab.Term.FunBinders.State
-- Init.Data.Nat.Lemmas
Nat.one_lt_succ_succ : ∀ (n : ℕ), 1 < n.succ.succ
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivWithinAt.sub` -/
HasFDerivWithinAt.fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt g g' s x → HasFDerivWithinAt (fun i => f i - g i) (f' - g') s x
-- Std.Http.Data.Headers
/-- Like `get?`, but panics if absent.
 -/
Std.Http.Headers.get! : Std.Http.Headers → Std.Http.Header.Name → Std.Http.Header.Value
-- Qq.Commands
/-- Build a let expression, similarly to `mkLetFVars`.
The array of `values` will be assigned to the current local context,
which is expected to consist of `cdecl`s.
 -/
_private.Qq.Commands.0.Qq.mkLetFVarsFromValues : Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Complex.Exponential
Complex.isCauSeq_exp : ∀ (z : ℂ), IsCauSeq (fun x => ‖x‖) fun n => ∑ m ∈ Finset.range n, z ^ m / ↑m.factorial
-- Mathlib.Order.LiminfLimsup
/-- A version of `le_limsup_iff` with large inequalities in densely ordered spaces.  -/
Filter.le_limsup_iff' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β}
  [DenselyOrdered β] {x : β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.le_limsup_iff'._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.le_limsup_iff'._auto_3 →
      (x ≤ Filter.limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a)
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.monotone_sum_take : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [CanonicallyOrderedAdd M] (L : List M),
  Monotone fun i => (List.take i L).sum
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.snd_map₂ : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  {f g : a ⟶ b} (a_1 : f ⟶ g), (CategoryTheory.Bicategory.Prod.snd B C).map₂ a_1 = a_1.2
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
ContinuousMap.Homotopy.ulift_apply : ∀ {X Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) (i : ULift.{u, 0} ↑unitInterval) (x : ↑X),
  H.uliftMap (i, x) = H (i.down, x)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- The notation for rational maps.  -/
AlgebraicGeometry.«term_⤏_» : Lean.TrailingParserDescr
-- Mathlib.Data.Finsupp.Defs
Finsupp.coe_mk : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (f : α → M) (s : Finset α) (h : ∀ (a : α), a ∈ s ↔ f a ≠ 0),
  ⇑{ support := s, toFun := f, mem_support_toFun := h } = f
-- Init.Data.UInt.Lemmas
UInt16.ofNatTruncate_toNat : ∀ (n : UInt16), UInt16.ofNatClamp n.toNat = n
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem_toList_roo : ∀ {m n : ℤ} {i : ℕ} (_h : i < (m<...n).toList.length), (m<...n).toList[i] = m + 1 + ↑i
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.Hom.mk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v, u₂} D] →
      {F : C → D} → {X Y : CategoryTheory.InducedCategory D F} → (F X ⟶ F Y) → X.Hom Y
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntry?ₘ'.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (motive : (Std.DTreeMap.Internal.Impl.ExplorationStep α β fun x => Ordering.lt) → Sort u_3) →
        (step : Std.DTreeMap.Internal.Impl.ExplorationStep α β fun x => Ordering.lt) →
          ((ky : α) →
              (a : Ordering.lt = Ordering.lt) →
                (y : β ky) →
                  (a_1 : List ((a : α) × β a)) → motive (Std.DTreeMap.Internal.Impl.ExplorationStep.lt ky a y a_1)) →
            ((a : List ((a : α) × β a)) →
                (a_1 : Std.DTreeMap.Internal.Cell α β fun x => Ordering.lt) →
                  (r : List ((a : α) × β a)) → motive (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_1 r)) →
              motive step
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.length_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.keys.length = t.size
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.PartialMap.comp_assoc : ∀ {X₁ X₂ X₃ Y : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X₁] [inst_1 : IrreducibleSpace ↥X₂]
  [inst_2 : Nonempty ↥X₃] (f : X₁.PartialMap X₂) [inst_3 : AlgebraicGeometry.IsDominant f.hom] (g : X₂.PartialMap X₃)
  [inst_4 : AlgebraicGeometry.IsDominant g.hom] (h : X₃.PartialMap Y), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.AbsolutelyContinuous.support_mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ ν : MeasureTheory.Measure X},
  μ.AbsolutelyContinuous ν → μ.support ⊆ ν.support
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.frobenius_pow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K] {p : ℕ} [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP K p]
  {n : ℕ}, Fintype.card K = p ^ n → frobenius K p ^ n = 1
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.unit_mul_pow_congr_unit : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] {ϖ : R},
  Irreducible ϖ → ∀ (u v : Rˣ) (m n : ℕ), ↑u * ϖ ^ m = ↑v * ϖ ^ n → u = v
-- Init.Data.Fin.Fold
Fin.foldrM_succ : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (f : Fin (n + 1) → α → m α),
  Fin.foldrM (n + 1) f = fun x => Fin.foldrM n (fun i => f i.succ) x >>= f 0
-- Mathlib.Order.Filter.CountableInter
Filter.CountableGenerateSets.below.basic : ∀ {α : Type u_2} {g : Set (Set α)} {motive : (a : Set α) → Filter.CountableGenerateSets g a → Prop} {s : Set α}
  (a : s ∈ g), Filter.CountableGenerateSets.below ⋯
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_set : ∀ {M : Type u_4} [inst : AddMonoid M] (L : List M) (n : ℕ) (a : M),
  (L.set n a).sum = ((List.take n L).sum + if n < L.length then a else 0) + (List.drop (n + 1) L).sum