mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.compose : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {l1 : α → β}
  {u1 : β → α} {l2 : β → γ} {u2 : γ → β},
  GaloisConnection l1 u1 → GaloisConnection l2 u2 → GaloisConnection (l2 ∘ l1) (u1 ∘ u2)
-- Init.Data.Int.DivMod.Lemmas
Int.natCast_eq_zero : ∀ {n : ℕ}, ↑n = 0 ↔ n = 0
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toArray_toList : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {it : Std.IterM m β}, List.toArray <$> it.toList = it.toArray
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.isoMk_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C}
  (e : X.toPresheafedSpace ≅ Y.toPresheafedSpace),
  (AlgebraicGeometry.SheafedSpace.isoMk e).inv = CategoryTheory.InducedCategory.homMk e.inv
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind : Type
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.HasLift.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g}, Nonempty sq.LiftStruct → sq.HasLift
-- Mathlib.Algebra.DirectSum.Module
DirectSum.mrange_map : ∀ {ι : Type v} {M : ι → Type w} [inst : (i : ι) → AddCommMonoid (M i)] {N : ι → Type u_1}
  [inst_1 : (i : ι) → AddCommMonoid (N i)] (f : (i : ι) → M i →+ N i),
  AddMonoidHom.mrange (DirectSum.map f) =
    AddSubmonoid.comap (DirectSum.coeFnAddMonoidHom N) (AddSubmonoid.pi Set.univ fun i => AddMonoidHom.mrange (f i))
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [Countable ι] (hτ : MeasureTheory.IsStoppingTime f τ) (i : ι), MeasurableSet {ω | ↑i ≤ τ ω}
-- Mathlib.Algebra.Module.ZLattice.Covolume
/-- The covolume of a `ℤ`-lattice is the volume of some fundamental domain; see
`ZLattice.covolume_eq_volume` for the proof that the volume does not depend on the choice of
the fundamental domain.  -/
ZLattice.covolume : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : MeasurableSpace E] → Submodule ℤ E → autoParam (MeasureTheory.Measure E) ZLattice.covolume._auto_1 → ℝ
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instLargeCategory : CategoryTheory.LargeCategory SFinKer
-- Mathlib.Data.Multiset.Sort
Multiset.instToExprOfToLevel : {α : Type u} → [Lean.ToLevel] → [Lean.ToExpr α] → Lean.ToExpr (Multiset α)
-- Init.Data.List.Monadic
List.forIn'.loop.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α)
  (f : (a : α) → a ∈ as → β → m (ForInStep β)) (b : β) (x_3 : ∃ bs, bs ++ [] = as),
  List.forIn'.loop as f [] b x_3 = pure b
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.units_rank_eq_units_rank : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [NumberField.IsCMField K] [inst_3 : NumberField K],
  NumberField.Units.rank ↥(NumberField.maximalRealSubfield K) = NumberField.Units.rank K
-- Mathlib.Order.WellFounded
/-- Let `r` be a relation on `α`, let `C : α → Prop` and let `bot : α`.
This induction principle shows that `C bot` holds, given that
* some `a` that is accessible by `r` satisfies `C a`, and
* for each `b ≠ bot` such that `C b` holds, there is `c` satisfying `r c b` and `C c`.  -/
Acc.induction_bot : ∀ {α : Sort u_4} {r : α → α → Prop} {a bot : α},
  Acc r a → ∀ {C : α → Prop}, (∀ (b : α), b ≠ bot → C b → ∃ c, r c b ∧ C c) → C a → C bot
-- Mathlib.MeasureTheory.Measure.Restrict
/-- **Alias** of `MeasureTheory.Measure.restrict_inter_add_sdiff₀`. -/
MeasureTheory.Measure.restrict_inter_add_diff₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasureTheory.NullMeasurableSet t μ → μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.insertMany_list_singleton : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {k : α} {v : β k}
  [EquivBEq α] [LawfulHashable α], m.WF → m.insertMany [⟨k, v⟩] = m.insert k v
-- Mathlib.Data.List.Chain
List.IsChain.iff : ∀ {α : Type u_1} {R S : α → α → Prop},
  (∀ (a b : α), R a b ↔ S a b) → ∀ {l : List α}, List.IsChain R l ↔ List.IsChain S l
-- Mathlib.Data.Set.Function
Set.InjOn.image_eq_image_iff : ∀ {α : Type u_1} {β : Type u_2} {s s₁ s₂ : Set α} {f : α → β},
  Set.InjOn f s → s₁ ⊆ s → s₂ ⊆ s → (f '' s₁ = f '' s₂ ↔ s₁ = s₂)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
/-- `2` is a square modulo an odd prime `p` iff `p` is congruent to `1` or `7` mod `8`.  -/
ZMod.exists_sq_eq_two_iff : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], p ≠ 2 → (IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7)
-- Mathlib.LinearAlgebra.Span.Basic
/-- Version of `disjoint_span_singleton` that works when the scalars are not a field.  -/
Submodule.disjoint_span_singleton'' : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s : Submodule R M}
  {x : M}, Disjoint s (R ∙ x) ↔ ∀ (r : R), r • x ∈ s → r • x = 0
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.precomp_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Z : Type v'} [inst_1 : TopologicalSpace Z]
  {T : Type v''} [inst_2 : TopologicalSpace T] {i : ι} (f : C(X i, Z)) (g : Topology.ContinuousMapGeneratedBy X Z T),
  ⇑(Topology.ContinuousMapGeneratedBy.precomp f g) = ⇑g ∘ ⇑f
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.fst_prod_snd : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B],
  (ContinuousAlgHom.fst R A B).prod (ContinuousAlgHom.snd R A B) = ContinuousAlgHom.id R (A × B)
-- Mathlib.Data.Sym.Sym2
Set.sym2_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, (f ⁻¹' s).sym2 = Sym2.map f ⁻¹' s.sym2
-- Mathlib.Algebra.Order.Group.Synonym
isAddLeftRegular_toLex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : α}, IsAddLeftRegular (toLex a) ↔ IsAddLeftRegular a
-- Batteries.Data.Nat.Basic
Nat.instNeZeroHPowOfNat_batteries : ∀ {n : ℕ}, NeZero (n ^ 0)
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk_dual : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M], CommRing.Pic.mk R (Module.Dual R M) = (CommRing.Pic.mk R M)⁻¹
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_eq_bot_iff : ∀ {ι : Type u_5} {α : Type u_7} [inst : LinearOrder α] [inst_1 : BoundedOrder α] [Nontrivial α] {s : Finset ι}
  {f : ι → α}, s.inf f = ⊥ ↔ ∃ b ∈ s, f b = ⊥
-- Mathlib.LinearAlgebra.Complex.Module
/-- We need this lemma since `Complex.coe_algebraMap` diverts the simp-normal form away from
`AlgHom.commutes`.  -/
AlgHom.map_coe_real_complex : ∀ {A : Type u_3} [inst : Semiring A] [inst_1 : Algebra ℝ A] (f : ℂ →ₐ[ℝ] A) (x : ℝ), f ↑x = (algebraMap ℝ A) x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = false → t.get? a = none
-- Mathlib.Data.Finset.Density
Finset.dens_ne_zero : ∀ {α : Type u_2} [inst : Fintype α] {s : Finset α}, s.dens ≠ 0 ↔ s.Nonempty
-- Mathlib.Data.Set.Function
Set.mapsTo_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.MapsTo f s ∅ ↔ s = ∅
-- Mathlib.Order.Sublocale
Sublocale.mk : {X : Type u_2} →
  [inst : Order.Frame X] →
    (carrier : Set X) → (∀ s ⊆ carrier, sInf s ∈ carrier) → (∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier) → Sublocale X
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
MDifferentiableWithinAt.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : M → M') (s : Set M) (x : M),
  MDiffAt[s] f x = ChartedSpace.LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x
-- Mathlib.Data.Set.Card
Set.ncard_congr' : ∀ {α : Type u_1} {β : Type u_2} {S : Set α} {T : Set β} (f : ↑S ≃ ↑T), S.ncard = T.ncard
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryLT : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) →
          (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.Ordered → (∃ a ∈ t, compare a k = Ordering.lt) → α × β
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_apply_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set (α × β)},
  MeasurableSet s → (μ.prod ν) s = ∫⁻ (y : β), μ ((fun x => (x, y)) ⁻¹' s) ∂ν
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- **The (little) ℓᵖ space**: The additive subgroup of a type synonym of `Π i, E i`, which consists
of those functions `f` such that `Memℓp f p` (i.e., `f` has finite `p`-norm).

The non-dependent version comes equipped with the notation `ℓ^p(ι, E)` in the `lp` namespace. When
`p` takes the values `0`, `1` or `2`, the notation `ℓ⁰(ι, E)`, `ℓ¹(ι, E)`, `ℓ²(ι, E)` is also
available.  -/
lp : {α : Type u_3} → (E : α → Type u_5) → [inst : (i : α) → NormedAddCommGroup (E i)] → ENNReal → AddSubgroup (PreLp E)
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_pow : ∀ {R : Type u} {α : Type u_1} [inst : SMul α R] (x : Tropical R) (n : α),
  Tropical.untrop (x ^ n) = n • Tropical.untrop x
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.PullbackCone.combine_pt_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} (f : F ⟶ H) (g : G ⟶ H)
  (c : (X : D) → CategoryTheory.Limits.PullbackCone (f.app X) (g.app X))
  (hc : (X : D) → CategoryTheory.Limits.IsLimit (c X)) {X Y : D} (h : X ⟶ Y),
  (CategoryTheory.Limits.PullbackCone.combine f g c hc).pt.map h =
    (hc Y).lift
      { pt := (c X).pt,
        π :=
          CategoryTheory.CategoryStruct.comp (c X).π
            (CategoryTheory.Limits.cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯) }
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_eq_max' : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a * b → a * b = max a b
-- Lean.Elab.WhereFinally
Lean.Elab.WhereFinallyView.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (tactic : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq),
  sizeOf { ref := ref, tactic := tactic } = 1 + sizeOf ref + sizeOf tactic
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromSource.instIsomorphismsOfIsClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms], P.InheritedFromSource (CategoryTheory.MorphismProperty.isomorphisms C)
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainGoal.mk.injEq : ∀ (rendered : String) (goals : Array String) (rendered_1 : String) (goals_1 : Array String),
  ({ rendered := rendered, goals := goals } = { rendered := rendered_1, goals := goals_1 }) =
    (rendered = rendered_1 ∧ goals = goals_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_filter_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {f : α → β → Bool} {k k' : α},
  t.getKey? k = some k' →
    Std.DTreeMap.Const.get! (Std.DTreeMap.filter f t) k =
      (Option.filter (fun x => f k' x) (Std.DTreeMap.Const.get? t k)).get!
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.app_eq_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens},
  AlgebraicGeometry.Scheme.Hom.app f U =
    AlgebraicGeometry.Scheme.Hom.appLE f U ((TopologicalSpace.Opens.map f.base).obj U) ⋯
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.innerRegular_neg_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G], μ.neg.InnerRegular ↔ μ.InnerRegular
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.isMin_of_noMax : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α],
  Order.IsSuccPrelimit a → IsMin a
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.order_finite_iff_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, φ.order < ⊤ ↔ φ ≠ 0
-- Mathlib.Geometry.Manifold.BumpFunction
/-- Replace `rIn` with another value in the interval `(0, f.rOut)`.  -/
SmoothBumpFunction.updateRIn : {E : Type uE} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type uH} →
        [inst_2 : TopologicalSpace H] →
          {I : ModelWithCorners ℝ E H} →
            {M : Type uM} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  {c : M} → (f : SmoothBumpFunction I c) → (r : ℝ) → r ∈ Set.Ioo 0 f.rOut → SmoothBumpFunction I c
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- A star projection operator is positive.

The proof of this will soon be simplified to `IsStarProjection.nonneg` when we
have `StarOrderedRing (E →L[𝕜] E)`.  -/
ContinuousLinearMap.IsPositive.of_isStarProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {p : E →L[𝕜] E}, IsStarProjection p → p.IsPositive
-- Init.Data.UInt.Lemmas
UInt8.toUSize_ofNatClamp_of_le : ∀ {n : ℕ}, UInt8.size ≤ n → (UInt8.ofNatClamp n).toUSize = USize.ofNatLT (UInt8.size - 1) ⋯
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The empty set is coplanar.  -/
coplanar_empty : ∀ (k : Type u_1) {V : Type u_2} (P : Type u_3) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P], Coplanar k ∅
-- Mathlib.Topology.ContinuousOn
ContinuousOn.preimage_interior_subset_interior_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {t : Set β}, ContinuousOn f s → IsOpen s → s ∩ f ⁻¹' interior t ⊆ s ∩ interior (f ⁻¹' t)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialLeftAdjointHomEquiv_symm_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) {X : F.PartialLeftAdjointSource} {Y Y' : D} (f : X.obj ⟶ F.obj Y) (g : Y ⟶ Y')
  {Z : D} (h : Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.partialLeftAdjointHomEquiv.symm f) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp
      (F.partialLeftAdjointHomEquiv.symm (CategoryTheory.CategoryStruct.comp f (F.map g))) h
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.completeTheory.isComplete : ∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M] [Nonempty M], (L.completeTheory M).IsComplete
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_eq_false_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {k : α},
  m.contains k = false ↔ k ∉ m
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.iteratedFDerivComponent_apply : ∀ {𝕜 : Type u} {ι : Type v} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] {α : Type u_1}
  [inst_6 : Fintype α] (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ ↑s)
  [inst_7 : DecidablePred fun x => x ∈ s] (v : (i : { a // a ∉ s }) → E₁ ↑i) (w : α → (i : ι) → E₁ i),
  ((f.iteratedFDerivComponent e) v) w = f fun j => if h : j ∈ s then w (e.symm ⟨j, h⟩) j else v ⟨j, h⟩
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.maxKey!_modify_eq_maxKey! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Raw.Const.modify t k f).maxKey! = t.maxKey!
-- Lean.Server.Requests
Lean.Server.instInhabitedServerRequestResponse : {a : Type} → Inhabited (Lean.Server.ServerRequestResponse a)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.core.sizeOf_spec : ∀ (a b : Lean.Expr) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.core a b lhs rhs) =
    1 + sizeOf a + sizeOf b + sizeOf lhs + sizeOf rhs
-- Mathlib.Topology.Instances.RatLemmas
Rat.not_countably_generated_cocompact : ¬(Filter.cocompact ℚ).IsCountablyGenerated
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumElim_add : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddZeroClass M] (a b : α →₀ M) (c d : β →₀ M),
  (a + b).sumElim (c + d) = a.sumElim c + b.sumElim d
-- Std.Sync.Broadcast
/-- Dequeues an element from the front of the circular buffer.
Returns none if the buffer is empty.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.dequeue : {α : Type} → Std.Bounded.State✝ α → Std.Bounded.State✝ α
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.mem_distTriang_op_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔
    Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles
-- Std.Async.ContextAsync
/-- Launches a `ContextAsync` computation in the background, discarding its result.

The computation runs independently in the background in its own child context. The parent computation does not wait
for background tasks to complete. This means that if the parent finishes its execution it will cause
the cancellation of the background functions. See also `disown` for launching tasks that continue independently
even after parent cancellation.
 -/
Std.Async.ContextAsync.background : {α : Type} → Std.Async.ContextAsync α → optParam Task.Priority Task.Priority.default → Std.Async.ContextAsync Unit
-- Mathlib.Data.List.Lattice
List.inter_nil' : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l ∩ [] = []
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
/-- Given an iterator `it` and a monadic predicate `P`, `it.dropWhileM P` is an iterator that
emits the values emitted by `it` starting from the first value that is rejected by `P`.
The elements before are dropped.

If `P` is pure, then the simpler variant `dropWhile` can be used instead.

**Marble diagram (ignoring monadic effects):**

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

```text
it                ---a----b---c--d-e--⊥
it.dropWhileM P   ------------c--d-e--⊥

it                ---a----⊥
it.dropWhileM P   --------⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite

Depending on `P`, it is possible that `it.dropWhileM P` is finite (or productive) although
`it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved manually.

**Performance:**

This combinator calls `P` on each output of `it` until the predicate evaluates to false. After
that, the combinator incurs an addictional O(1) cost for each value emitted by `it`.
 -/
Std.IterM.dropWhileM : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [Monad m] → [inst : MonadAttach m] → (P : β → m (ULift.{w, 0} Bool)) → Std.IterM m β → Std.IterM m β
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNNNorm_mulVec : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n),
  ‖(EuclideanSpace.equiv m 𝕜).symm (A.mulVec x.ofLp)‖₊ ≤ ‖A‖₊ * ‖x‖₊
-- Lean.Parser.Term
/-- This is the same as `byTactic`, but it uses a different syntax kind. This is
used by `show` and `suffices` instead of `byTactic` because these syntaxes don't
support arbitrary terms where `byTactic` is accepted. Mathport uses this to e.g.
safely find-replace `by exact $e` by `$e` in any context without causing
incorrect syntax when the full expression is `show $T by exact $e`.
 -/
Lean.Parser.Term.byTactic' : Lean.Parser.Parser
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_eq_get_get? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (h : m.WF) {a : α} {h' : a ∈ m}, m.get a h' = (m.get? a).get ⋯
-- Std.Time.Format.Modifier
/-- `e`: Day of week as number or text (e.g., 1, 01, Mon, Monday, M).
The numeric value uses Monday=1 through Sunday=7 (ISO 8601 convention).
Text output is the same as `E`.
 -/
Std.Time.Modifier.e : Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K : HomologicalComplex₂ C c₁ c₂}
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {A : C} {i₁₂ : I₁₂} {f g : (K.total c₁₂).X i₁₂ ⟶ A},
  (∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
      CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) f =
        CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) g) →
    f = g
-- Aesop.Script.UScriptToSScript
_private.Aesop.Script.UScriptToSScript.0.Aesop.Script.StepTree.numSiblings.go : {σ : Type} → ℕ → Aesop.Script.StepTree → StateRefT' σ (Std.HashMap Lean.MVarId ℕ) (ST σ) Unit
-- Mathlib.AlgebraicGeometry.Fiber
/-- The `κ(x)`-point of `f ⁻¹' {f x}` corresponding to `x`.  -/
AlgebraicGeometry.Scheme.Hom.asFiberHom : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → (x : ↥X) → AlgebraicGeometry.Spec (X.residueField x) ⟶ AlgebraicGeometry.Scheme.Hom.fiber f (f x)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
_private.Mathlib.Analysis.BoxIntegral.UnitPartition.0.BoxIntegral.unitPartition.tendsto_card_div_pow₆ : ∀ {ι : Type u_1} (s : Set (ι → ℝ)) [inst : Fintype ι],
  (fun x =>
      ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ Fintype.card ι *
        (↑⌈x⌉₊ / x) ^ Fintype.card ι) =ᶠ[Filter.atTop]
    fun x => ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ Fintype.card ι
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.join_map_dirac : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  (MeasureTheory.Measure.map MeasureTheory.Measure.dirac μ).join = μ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.of_sub_left : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, (s - t).Nonempty → s.Nonempty