mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Transitive
IsOpen.dense_iUnion_smul : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α]
  [h : MulAction.IsTopologicallyTransitive M α] {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ m, m • U)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqMon.beq_spec_2 : ∀ (a : Lean.Grind.CommRing.Power) (a_1 : Lean.Grind.CommRing.Mon) (b : Lean.Grind.CommRing.Power)
  (b_1 : Lean.Grind.CommRing.Mon),
  (Lean.Grind.CommRing.Mon.mult a a_1 == Lean.Grind.CommRing.Mon.mult b b_1) = (a == b && a_1 == b_1)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_pointReflection_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), midpoint R ((Equiv.pointReflection x) y) y = x
-- Mathlib.RingTheory.MvPowerSeries.LinearTopology
MvPowerSeries.LinearTopology.isTopologicallyNilpotent_of_constantCoeff : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R]
  {f : MvPowerSeries σ R}, IsTopologicallyNilpotent (MvPowerSeries.constantCoeff f) → IsTopologicallyNilpotent f
-- Mathlib.Data.Finset.NAry
Finset.image₂_empty_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {t : Finset β},
  Finset.image₂ f ∅ t = ∅
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffAt.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℝ n f x → ContDiffAt ℝ n (fun x => Real.cosh (f x)) x
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_pow_sub_sub : ∀ {E' : Type u_6} [inst : SeminormedAddCommGroup E'] (x₀ : E') {m : ℕ},
  1 < m → (fun x => ‖x - x₀‖ ^ m) =o[nhds x₀] fun x => x - x₀
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linearMapAt_eq_zero : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] {b : B},
  b ∉ e.baseSet → Bundle.Pretrivialization.linearMapAt R e b = 0
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `sub_apply`. -/
CuspForm.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.isFiniteMeasure_of_forall_abs_le : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] {C : ℝ},
  (∀ (x : R), |↑f x| ≤ C) → MeasureTheory.IsFiniteMeasure f.measure
-- Mathlib.Data.List.TakeWhile
List.find?_not_eq_head?_dropWhile : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.find? (fun x => !p x) l = (List.dropWhile p l).head?
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.Scheme.germToFunctionField.congr_simp : ∀ (X : AlgebraicGeometry.Scheme) [inst : IrreducibleSpace ↥X] (U : X.Opens) [h : Nonempty ↥↑U],
  X.germToFunctionField U = X.germToFunctionField U
-- Lean.Parser.Level
Lean.Parser.Level.imax.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Sat.CNF.Basic
Std.Sat.CNF.clauses : {α : Type u} → Std.Sat.CNF α → Array (Std.Sat.CNF.Clause α)
-- Mathlib.Algebra.Exact.Basic
LinearEquiv.postcomp_exact_iff_exact : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} {P' : Type u_7} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid P']
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R P'] {f : M →ₗ[R] N}
  {g : N →ₗ[R] P} {e : P ≃ₗ[R] P'}, Function.Exact ⇑f ⇑(↑e ∘ₗ g) ↔ Function.Exact ⇑f ⇑g
-- Mathlib.Algebra.Algebra.Unitization
Unitization.snd_inr : ∀ (R : Type u_1) {A : Type u_2} [inst : Zero R] (a : A), (↑a).toProd.2 = a
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_self : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R], MvPowerSeries.subst MvPowerSeries.X = id
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : β k → β k}, (t.modify k f).contains k' = t.contains k'
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_zero : ∀ {M : Type u_10} {F : Type u_11} [inst : Zero M] [inst_1 : FunLike F M M] [ZeroHomClass F M M] (f : F) (n : ℕ),
  (⇑f)^[n] 0 = 0
-- Init.Prelude
Complement.mk : {α : Type u} → (α → α) → Complement α
-- Mathlib.NumberTheory.GaussSum
/-- The Gauss sum of a nontrivial multiplicative character and the trivial additive character
vanishes.  -/
gaussSum_one_right : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : Fintype R] [inst_2 : CommRing R'] [IsDomain R']
  {χ : MulChar R R'}, χ ≠ 1 → gaussSum χ 1 = 0
-- Mathlib.Data.Rat.Init
Rat.cast_id : ∀ (n : ℚ), ↑n = n
-- Init.Data.String.Basic
String.Slice.Pos.offset_add_slice : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}, p₀.offset + s.slice p₀ p₁ h = p₁.offset
-- Lean.Meta.Tactic.Grind.Types
/-- Case-splits that have already been performed, or that do not have to be performed anymore.  -/
Lean.Meta.Grind.Split.State.resolved : Lean.Meta.Grind.Split.State → Lean.PHashSet Lean.Meta.Sym.ExprPtr
-- Std.Time.Format
/-- Formats a `PlainTime` value into a 12-hour format string (`hh:mm:ss aa`).
 -/
Std.Time.PlainTime.toTime12Hour : Std.Time.PlainTime → String
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.comp.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {T : Type u_2} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι),
  Q.comp P =
    { val := Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val),
      σ' := fun x =>
        (Q.σ x).coeff.sum fun n r =>
          (MvPolynomial.rename Sum.inr) (P.σ r) * (MvPolynomial.monomial (Finsupp.mapDomain Sum.inl n)) 1,
      aeval_val_σ' := ⋯, algebraMap_eq := ⋯ }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonHoverParams.toJson : Lean.Lsp.HoverParams → Lean.Json
-- Lean.Data.Options
_private.Lean.Data.Options.0.Lean.Options.mk : Lean.NameMap Lean.DataValue → Bool → Lean.Options
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} {α β : F ⟶ G} (h : α = β)
  (X : CategoryTheory.Endofunctor.Algebra G),
  ((CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq h).hom.app X).f = CategoryTheory.CategoryStruct.id X.a
-- Init.Data.Range.Polymorphic.PRange
Std.Rcc.mk.inj : ∀ {α : Type u} {lower upper lower_1 upper_1 : α},
  ((lower...=upper) = lower_1...=upper_1) → lower = lower_1 ∧ upper = upper_1
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.compMeasurePreserving_val : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β} {f : α → β}
  (g : ↥(MeasureTheory.Lp E p μb)) (hf : MeasureTheory.MeasurePreserving f μ μb),
  ↑((MeasureTheory.Lp.compMeasurePreserving f hf) g) = (↑g).compMeasurePreserving f hf
-- Aesop.Frontend.Tactic
Aesop.Frontend.elabSimpConfigCtx : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Simp.ConfigCtx
-- Mathlib.Topology.Algebra.Algebra
instContinuousMulElemIooOfNat : ∀ (A : Type u) [inst : Semiring A] [inst_1 : TopologicalSpace A] [inst_2 : PartialOrder A]
  [inst_3 : IsStrictOrderedRing A] [ContinuousMul A], ContinuousMul ↑(Set.Ioo 0 1)
-- Mathlib.Combinatorics.Graph.Delete
Graph.deleteEdges_isLoopAt : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {F : Set β},
  (G.deleteEdges F).IsLoopAt e x ↔ G.IsLoopAt e x ∧ e ∉ F
-- Mathlib.Topology.Constructible
IsRetrocompact.sInter : ∀ {X : Type u_2} [inst : TopologicalSpace X] [T2Space X] {S : Set (Set X)},
  S.Finite → (∀ s ∈ S, IsRetrocompact s) → IsRetrocompact (⋂₀ S)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_minKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey?.isSome = true ↔ t.isEmpty = false
-- Init.Data.BitVec.Bitblast
BitVec.carry_succ : ∀ {w : ℕ} (i : ℕ) (x y : BitVec w) (c : Bool),
  BitVec.carry (i + 1) x y c = (x.getLsbD i).atLeastTwo (y.getLsbD i) (BitVec.carry i x y c)
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.prime_of_isIntegrallyClosed : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {x : S}, IsIntegral R x → Prime (minpoly R x)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaGrpObjObjEquiv_symm_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Grp C} {Y Y' : C} (g : Y' ⟶ Y)
  (f : Y ⟶ M.X),
  CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g f) =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaGrp.{w, v, u}.obj M).map g.op))
      (CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm f)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.add_fst : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : AddCommGroup β]
  (x y : WithLp p (α × β)), (x + y).fst = x.fst + y.fst
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- The (Loewner) partial order on linear maps on a Hilbert space determined by `f ≤ g`
if and only if `g - f` is a positive linear map (in the sense of `LinearMap.IsPositive`).  -/
LinearMap.instLoewnerPartialOrder : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → PartialOrder (E →ₗ[𝕜] E)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.tendsto_pow_log_div_mul_add_atTop : ∀ (a b : ℝ) (n : ℕ), a ≠ 0 → Filter.Tendsto (fun x => Real.log x ^ n / (a * x + b)) Filter.atTop (nhds 0)
-- Lean.Elab.Quotation
/-- Elaborate the content of a syntax quotation term  -/
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.quoteSyntax : Lean.Syntax → Lean.Elab.TermElabM Lean.Term
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- If `C` is an ordinary enriched category, the category structure on `TransportEnrichment F C`
is trivially equivalent to the one on `C` itself.  -/
CategoryTheory.TransportEnrichment.ofOrdinaryEnrichedCategoryEquiv : {V : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u) →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          {W : Type u''} →
            [inst_3 : CategoryTheory.Category.{v'', u''} W] →
              [inst_4 : CategoryTheory.MonoidalCategory W] →
                (F : CategoryTheory.Functor V W) → [inst_5 : F.LaxMonoidal] → CategoryTheory.TransportEnrichment F C ≌ C
-- Mathlib.Tactic.Ring.Common
/-- `ExSum BaseType sα e` stores the structure of a normalized polynomial expression `e`, which is
a sum of monomials.  -/
Mathlib.Tactic.Ring.Common.ExSum : {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Q(CommSemiring «$α») → Q(«$α») → Type
-- Mathlib.Order.Lattice
/-- **Alias** of the forward direction of `inf_eq_right`. -/
le_of_inf_eq' : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = b → b ≤ a
-- Mathlib.Data.PNat.Prime
Nat.Primes.coe_pnat_injective : Function.Injective Nat.Primes.toPNat
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.over_over : ∀ (n : Type u) (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.AffineSpace n S ↘ S =
    CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from S)
      (CategoryTheory.Limits.terminal.from (AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ)))))
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.baseChange_toGenerators : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (T : Type u_1) [inst_3 : CommRing T] [inst_4 : Algebra R T] (P : Algebra.Presentation R S ι σ),
  (Algebra.Presentation.baseChange T P).toGenerators = Algebra.Generators.baseChange T P.toGenerators
-- Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
LinearEquiv.conjAlgEquiv_surjective : ∀ (K : Type u_1) (V : Type u_2) (W : Type u_3) [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V] [inst_4 : AddCommMonoid W] [inst_5 : Module K W] [Module.Projective K W],
  Function.Surjective (LinearEquiv.conjAlgEquiv K)
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
bounded by `C`, then the function is `C`-Lipschitz. Version with `deriv`.  -/
Convex.norm_image_sub_le_of_norm_deriv_le : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : 𝕜 → G}
  {s : Set 𝕜} {x y : 𝕜} {C : ℝ},
  (∀ x ∈ s, DifferentiableAt 𝕜 f x) →
    (∀ x ∈ s, ‖deriv f x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.forget_preservesLimits : ∀ {R : Type u} [inst : CommRing R], CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget (AlgCat R))
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_mod : ∀ {a b : UInt16}, (a % b).toBitVec = a.toBitVec % b.toBitVec
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {Q : CategoryTheory.ObjectProperty C}
  [Q.IsClosedUnderIsomorphisms] [∀ (a : α), Q.IsClosedUnderColimitsOfShape (J a)], P ≤ Q → P.colimitsClosure J ≤ Q
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The type of homotopies between morphisms of simplicial sets relatively to
given subcomplexes. (See also `SSet.Homotopy` in the file
`Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean` for the non-relative version.)  -/
SSet.RelativeMorphism.Homotopy : {X Y : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} → {φ : A.toSSet ⟶ B.toSSet} → SSet.RelativeMorphism A B φ → SSet.RelativeMorphism A B φ → Type u
-- Mathlib.Topology.Order.ScottTopology
/-- Predicate for an ordered topological space to be equipped with its Scott-Hausdorff topology.

A set `u` is open in the Scott-Hausdorff topology iff when the least upper bound of a directed set
`d` lies in `u` then there is a tail of `d` which is a subset of `u`.

For mild conditions on `D`, this is equivalent to saying that open sets are `DirSupInaccOn D`,
and closed sets are `DirSupClosedOn D`.  -/
Topology.IsScottHausdorff : (α : Type u_3) → Set (Set α) → [Preorder α] → [TopologicalSpace α] → Prop
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isIso_hom : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F}
  (h : E.IsPointwiseRightKanExtension) [L.Full] [L.Faithful],
  CategoryTheory.IsIso (CategoryTheory.CostructuredArrow.hom E)
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourier_real_eq_integral_exp_smul : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (w : ℝ),
  FourierTransform.fourier f w = ∫ (v : ℝ), Complex.exp (↑(-2 * Real.pi * v * w) * Complex.I) • f v
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.quotientPi_aux.toFun : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {Ms : ι → Type u_3} →
        [inst_1 : (i : ι) → AddCommGroup (Ms i)] →
          [inst_2 : (i : ι) → Module R (Ms i)] →
            (p : (i : ι) → Submodule R (Ms i)) → ((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p → (i : ι) → Ms i ⧸ p i
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.containsThenInsertIfNew k v).1 = t.contains k
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddCancelMonoid α] {s : Finset α} {n : ℕ},
  n ≠ 0 → s.card ≤ (n • s).card
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- One direction of `mul_inv_le_iff₀` where `b` is allowed to be `0` (but `c` must be nonnegative).
 -/
mul_inv_le_of_le_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 ≤ b → 0 ≤ c → a ≤ c * b → a * b⁻¹ ≤ c
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerLeft_whiskerRight : ∀ (A : Type u_1) {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {F G : CategoryTheory.Functor B C} (η : F ⟶ G)
  (H : CategoryTheory.Functor C D),
  CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) (CategoryTheory.Functor.whiskerRight η H) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A F H).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) η)
          (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) H))
        (CategoryTheory.Join.mapCompRight A G H).inv)
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s t : Set α},
  μ s = 0 → ν t = 0 → Set.univ ⊆ s ∪ t → μ.MutuallySingular ν
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.quotientFunctor_map_cons : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {x y z : CategoryTheory.Paths V} (p : x ⟶ y) (q : y ⟶ z),
  (CategoryTheory.Cat.FreeRefl.quotientFunctor V).map (Quiver.Path.cons p q) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Cat.FreeRefl.quotientFunctor V).map p)
      (CategoryTheory.Cat.FreeRefl.homMk q)
-- Mathlib.Logic.Equiv.Fintype
Equiv.extendSubtype_not_mem : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] [inst_2 : Finite ↑{x | p x}]
  (e : { x // p x } ≃ { x // q x }) (x : α), ¬p x → ¬q (e.extendSubtype x)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `ι = ι'`, then `fork.ofι ι _` and `fork.ofι ι' _` are isomorphic.  -/
CategoryTheory.Limits.ofιCongr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {P : C} →
            {ι ι' : P ⟶ X} →
              {w : CategoryTheory.CategoryStruct.comp ι f = 0} →
                (h : ι = ι') → CategoryTheory.Limits.KernelFork.ofι ι w ≅ CategoryTheory.Limits.KernelFork.ofι ι' ⋯
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.index_apply : ∀ {ι : Type u_1} (m : ℕ) {x : ι → ℝ} (i : ι), BoxIntegral.unitPartition.index m x i = ⌈↑m * x i⌉ - 1
-- Mathlib.Algebra.Lie.OfAssociative
/-- Given an equivalence `e` of Lie algebras from `L` to `L'`, and an element `x : L`, the conjugate
of the endomorphism `ad(x)` of `L` by `e` is the endomorphism `ad(e x)` of `L'`.  -/
LieAlgebra.conj_ad_apply : ∀ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') (x : L),
  e.toLinearEquiv.conj ((LieAlgebra.ad R L) x) = (LieAlgebra.ad R L') (e x)
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.center_pi : ∀ {η : Type u_2} {G : η → Type u_3} [inst : (i : η) → AddGroup (G i)],
  AddSubgroup.center ((i : η) → G i) = AddSubgroup.pi Set.univ fun i => AddSubgroup.center (G i)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The range of a morphism of fields is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with `Subtype.Fintype` if `L` is also a fintype.  -/
RingHom.fintypeFieldRange : {K : Type u} →
  {L : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : DivisionRing L] → [Fintype K] → [DecidableEq L] → (f : K →+* L) → Fintype ↥f.fieldRange
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist_le : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), G.dist u v ≤ p.length
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCochain_fst : ∀ {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 φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m),
  (CochainComplex.mappingCone.liftCochain φ α β h).comp (↑(CochainComplex.mappingCone.fst φ)) h = α
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The fully faithful embedding `LightDiagram ⥤ Profinite`  -/
lightDiagramToProfinite : CategoryTheory.Functor LightDiagram Profinite
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.degree_of_notMem_verts : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v : V} [inst : Fintype ↑(G'.neighborSet v)],
  v ∉ G'.verts → G'.degree v = 0
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.IsLocallyFaithful.mk : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vD, uD} D]
  {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D},
  (∀ {U V : C} (f₁ f₂ : U ⟶ V),
      G.map f₁ = G.map f₂ →
        CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.equalizer f₁ f₂) ∈ K (G.obj U)) →
    G.IsLocallyFaithful K
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.card_S_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (A : Matrix α β ℤ) [inst_2 : DecidableEq α],
  ↑(Finset.Icc
          (fun i =>
            ∑ j,
              ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
                -(A i j)⁻)
          fun i =>
          ∑ j,
            ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
              (A i j)⁺).card =
    ∏ i,
      ((fun i =>
              ∑ j,
                ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
                  (A i j)⁺)
            i -
          (fun i =>
              ∑ j,
                ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ *
                  -(A i j)⁻)
            i +
        1)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_finset_def : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset β} {a : α},
  a • s = Finset.image (fun x => a • x) s