mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.mulConst_empty_left : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (B : Finset G), ∅.mulConst B = 0
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.inv_f_apply : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁ ⟶ C₂) [inst_2 : CategoryTheory.IsIso f] (j : ι), (CategoryTheory.inv f).f j = CategoryTheory.inv (f.f j)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).getD k' fallback =
        if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).getD fallback
        else t.getD k' fallback
-- Init.Data.BitVec.BasicAux
BitVec.instOfNat : {n i : ℕ} → OfNat (BitVec n) i
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_comp : ∀ {𝕜 : 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} {g : M → 𝕜} {u : Set M}
  {s : Set M'} (x : M'),
  MDiffAt[u] g (f x) →
    MDiffAt[s] f x → s ⊆ f ⁻¹' u → UniqueMDiffAt[s] x → d[s] (g ∘ f) x = d[u] g (f x) ∘SL mfderiv[s] f x
-- Init.Data.List.Lemmas
List.mem_concat_self : ∀ {α : Type u_1} {xs : List α} {a : α}, a ∈ xs ++ [a]
-- Lean.Elab.Term.TermElabM
/-- Auxiliary method for creating a `Syntax.ident` containing
a fresh name. This method is intended for creating fresh binder names.
It is just a thin layer on top of `mkFreshUserName`.  -/
Lean.Elab.Term.mkFreshIdent : {m : Type → Type} → [Monad m] → [Lean.MonadQuotation m] → Lean.Syntax → optParam Bool false → m Lean.Ident
-- Mathlib.Computability.NFA
/-- `M.toNFA` is an `NFA` constructed from a `DFA` `M` by using the same start and accept
states and a transition function which sends `s` with input `a` to the singleton `M.step s a`.  -/
DFA.toNFA : {α : Type u} → {σ : Type v} → DFA α σ → NFA α σ
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `UInt16.ofNat 5 = 5`
* `UInt16.ofNat 255 = 255`
* `UInt16.ofNat 32770 = 32770`
* `UInt16.ofNat 65537 = 1`
 -/
UInt16.ofNat : ℕ → UInt16
-- Aesop.Forward.State
Aesop.instHashableRawHyp.hash : Aesop.RawHyp → UInt64
-- Mathlib.LinearAlgebra.Dimension.Finite
iSupIndep.subtype_ne_bot_le_finrank_aux : ∀ {ι : Type w} {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] [Module.Finite R M] [StrongRankCondition R] {p : ι → Submodule R M},
  iSupIndep p → Cardinal.mk { i // p i ≠ ⊥ } ≤ ↑(Module.finrank R M)
-- Init.Data.Option.Lemmas
Option.none_or : ∀ {α : Type u_1} {o : Option α}, none.or o = o
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits.eq_def : ∀ {α : Type u_1} [inst : Semiring α] (b : α) (x : List ℕ),
  Nat.ofDigits b x =
    match x with
    | [] => 0
    | h :: t => ↑h + b * Nat.ofDigits b t
-- Mathlib.Topology.ContinuousMap.Polynomial
polynomialFunctions.starClosure_le_equalizer : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] {A : Type u_2}
  [inst_3 : StarRing R] [inst_4 : ContinuousStar R] [inst_5 : Semiring A] [inst_6 : StarRing A] [inst_7 : Algebra R A]
  (s : Set R) (φ ψ : C(↑s, R) →⋆ₐ[R] A),
  φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) →
    (polynomialFunctions s).starClosure ≤ StarAlgHom.equalizer φ ψ
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.top_toSubfield : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], ⊤.toSubfield = ⊤
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
_private.Mathlib.Geometry.Manifold.WhitneyEmbedding.0.SmoothBumpCovering.embeddingPiTangent_injective : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (↑⊤) M] [inst_7 : T2Space M] [inst_8 : Fintype ι]
  (f : SmoothBumpCovering ι I M), Function.Injective ⇑(SmoothBumpCovering.embeddingPiTangent✝ f)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.one.eq_1 : ∀ {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.one = Tactic.ComputeAsymptotics.MultiseriesExpansion.const basis 1
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.toContinuousLinearMap_toContinuousLinearEquiv_eq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), ↑↑e = (↑e).toContinuousLinearMap
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The type of blocks for a group action containing a given element  -/
MulAction.BlockMem : (G : Type u_1) → [inst : Group G] → {X : Type u_2} → [MulAction G X] → X → Type u_2
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.universalMulHom.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_2}
  [inst_2 : Monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)),
  OreLocalization.universalMulHom f fS hf =
    { toFun := fun x => OreLocalization.liftExpand (fun r s => ↑(fS s)⁻¹ * f r) ⋯ x, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.sectionsAddMonoid : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddMonCat) → AddMonoid ↑(F.comp (CategoryTheory.forget AddMonCat)).sections
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion within a set on a ball, then it is
continuous there.  -/
HasFPowerSeriesWithinOnBall.continuousOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → ContinuousOn f (insert x s ∩ Metric.eball x r)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.starClosure_eq_adjoin : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (S : NonUnitalSubalgebra R A), S.starClosure = NonUnitalStarAlgebra.adjoin R ↑S
-- Mathlib.Data.Set.Insert
Set.ssubset_iff_insert : ∀ {α : Type u_1} {s t : Set α}, s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- If `C` has products indexed by `X`, then `Cᵒᵖ` has coproducts indexed by `X`.
 -/
CategoryTheory.Limits.hasCoproductsOfShape_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Type v₂)
  [CategoryTheory.Limits.HasProductsOfShape X C], CategoryTheory.Limits.HasCoproductsOfShape X Cᵒᵖ
-- Mathlib.Logic.Function.Basic
Function.hasUncurryInduction : {α : Type u_1} →
  {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → [Function.HasUncurry β γ δ] → Function.HasUncurry (α → β) (α × γ) δ
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.poissonMeasure_real_singleton : ∀ (r : NNReal) (n : ℕ), (ProbabilityTheory.poissonMeasure r).real {n} = Real.exp (-↑r) * ↑r ^ n / ↑n.factorial
-- Lean.Elab.Level
Lean.Elab.Level.instAddMessageContextLevelElabM : Lean.AddMessageContext Lean.Elab.Level.LevelElabM
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionState.mk : {α : Type} →
  Array (Mathlib.Tactic.ClickSuggestions.Result α) →
    Array ProofWidgets.Html → Mathlib.Tactic.ClickSuggestions.SectionState α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.ofRepresentableBy_yonedaAddMonObjRepresentableBy : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.AddMonObj.ofRepresentableBy M (CategoryTheory.yonedaAddMonObj M)
      (CategoryTheory.yonedaAddMonObjRepresentableBy M) =
    inst_2
-- Mathlib.Algebra.Group.Prod
/-- Coproduct of two `AddMonoidHom`s with the same codomain:
`f.coprod g (p : M × N) = f p.1 + g p.2`.
(Commutative case; for the general case, see `AddHom.noncommCoprod`.)  -/
AddMonoidHom.coprod : {M : Type u_3} →
  {N : Type u_4} →
    {P : Type u_5} →
      [inst : AddZeroClass M] →
        [inst_1 : AddZeroClass N] → [inst_2 : AddCommMonoid P] → (M →+ P) → (N →+ P) → M × N →+ P
-- Lean.Meta.MkIffOfInductiveProp
/-- Apply the `n`-th constructor of the target type,
checking that it is an inductive type,
and that there are the expected number of constructors.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.MVarId.nthConstructor : Lean.Name → ℕ → optParam (Option ℕ) none → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.RingTheory.TensorProduct.Basic
/-- The ring morphism `A →+* A ⊗[R] B` sending `a` to `a ⊗ₜ 1`.  -/
Algebra.TensorProduct.includeLeftRingHom : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → A →+* TensorProduct R A B
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_tower'`.

---

See `ramificationIdx_tower` for a version that does not assume primality.  -/
Ideal.ramificationIdx'_tower' : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [inst_7 : q.IsPrime] [inst_8 : r.IsPrime] [inst_9 : r.LiesOver q]
  [inst_10 : Algebra (Localization.AtPrime q) (Localization.AtPrime r)] [Localization.AtPrime.IsLiesOverAlgebra q r]
  [Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)],
  r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
/-- The single functor `C ⥤ CochainComplex C ℤ` which sends `X` to the complex
consisting of `X` in degree `n : ℤ` and zero otherwise.
(This is definitionally equal to `HomologicalComplex.single C (up ℤ) n`,
but `singleFunctor C n` is the preferred term when interactions with shifts are relevant.)  -/
CochainComplex.singleFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasZeroObject C] → ℤ → CategoryTheory.Functor C (CochainComplex C ℤ)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- A `p`-th root of unity that is not `1`, with `p` prime, satisfies `IsPrimitiveRoot η p`.  -/
isPrimitiveRoot_of_mem_nthRootsFinset : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ},
  Nat.Prime p → ∀ {η : R}, η ∈ Polynomial.nthRootsFinset p 1 → η ≠ 1 → IsPrimitiveRoot η p
-- Mathlib.Algebra.Ring.InjSurj
AddOpposite.instHasDistribNeg : {R : Type u_1} → [inst : Mul R] → [HasDistribNeg R] → HasDistribNeg Rᵃᵒᵖ
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.toAddSubgroup_inf : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U V : OpenAddSubgroup G}, ↑(U ⊓ V) = ↑U ⊓ ↑V
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.inv_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → Group (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] (i : ι)
  (x : G i), (⟦⟨i, x⟩⟧)⁻¹ = ⟦⟨i, x⁻¹⟩⟧
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.exists_eq_pow_p_mul' : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [CharP k p] [PerfectRing k p] (a : WittVector p k),
  a ≠ 0 → ∃ m b, a = ↑p ^ m * ↑b
-- Lean.Parser.Term
/-- Specify a termination measure for recursive functions.
```
termination_by a - b
```
indicates that termination of the currently defined recursive function follows
because the difference between the arguments `a` and `b` decreases.

If the function takes further argument after the colon, you can name them as follows:
```
def example (a : Nat) : Nat → Nat → Nat :=
termination_by b c => a - b
```

By default, a `termination_by` clause will cause the function to be constructed using well-founded
recursion. The syntax `termination_by structural a` (or `termination_by structural _ c => c`)
indicates the function is expected to be structural recursive on the argument. In this case
the body of the `termination_by` clause must be one of the function's parameters.

If omitted, a termination measure will be inferred. If written as `termination_by?`,
the inferred termination measure will be suggested.

 -/
Lean.Parser.Termination.terminationBy? : Lean.Parser.Parser
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.mem_succ_succ_iff : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [DecidableLT α] [inst_3 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {lo hi a : α},
  (a ∈ (Std.PRange.succ lo)...Std.PRange.succ hi) ↔ ∃ a', a = Std.PRange.succ a' ∧ a' ∈ lo...hi
-- Std.Time.DateTime.WallTime
/-- A wall-clock time is what a clock shows in a given timezone: the local civil time at some point in
time. It is stored as a `Duration` since `1970-01-01T00:00:00` in local time, equivalent to a
`PlainDateTime` packed into a single offset, which makes arithmetic straightforward.

Every timezone induces a correspondence between `Timestamp` and `WallTime`: interpreting a
`Timestamp` in a timezone yields the `WallTime` (what a clock in that timezone reads at that
instant), and resolving a `WallTime` in a timezone yields the `Timestamp` (the absolute instant the
clock reading refers to).
 -/
Std.Time.WallTime : Type
-- Mathlib.Topology.EMetricSpace.Basic
EMetric.totallyBounded_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α},
  TotallyBounded s ↔ ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.eball y ε
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffWithinAt.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {s : Set G} {x : G} {n : WithTop ℕ∞},
  ContDiffWithinAt ℝ n f s x → ContDiffWithinAt ℝ n g s x → ContDiffWithinAt ℝ n (fun x => inner 𝕜 (f x) (g x)) s x
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
FiberBundle.trivializationAt_continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (x₀ : B)
  (x : Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x),
  ↑(trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂) (fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x) x₀) x =
    (x.proj, ContinuousAlternatingMap.inCoordinates F₁ F₂ x₀ x.proj x₀ x.proj x.snd)
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_biprod_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  P (X ⊞ Y) → P Y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constMergeWith : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ t₃ t₄ : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp],
  t₁.WF →
    t₂.WF →
      t₃.WF →
        t₄.WF →
          ∀ (f : α → β → β → β),
            t₁.Equiv t₂ →
              t₃.Equiv t₄ → (Std.DTreeMap.Raw.Const.mergeWith f t₁ t₃).Equiv (Std.DTreeMap.Raw.Const.mergeWith f t₂ t₄)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddBelow.neg : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G},
  BddBelow s → BddAbove (-s)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.negMulLog_le_one_sub_self : ∀ {x : ℝ}, 0 ≤ x → x.negMulLog ≤ 1 - x
-- Mathlib.Geometry.Manifold.ContMDiffMap
/-- Given two `C^n` maps `f` and `g`, this is the `C^n` map `x ↦ (f x, g x)`.  -/
ContMDiffMap.prodMk : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_5} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_6} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {F : Type u_11} →
                                          [inst_11 : NormedAddCommGroup F] →
                                            [inst_12 : NormedSpace 𝕜 F] →
                                              {G : Type u_12} →
                                                [inst_13 : TopologicalSpace G] →
                                                  {J : ModelWithCorners 𝕜 F G} →
                                                    {N : Type u_13} →
                                                      [inst_14 : TopologicalSpace N] →
                                                        [inst_15 : ChartedSpace G N] →
                                                          {n : WithTop ℕ∞} →
                                                            ContMDiffMap J I N M n →
                                                              ContMDiffMap J I' N M' n →
                                                                ContMDiffMap J (I.prod I') N (M × M') n
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset : ∀ {L : FirstOrder.Language} {ι : Type u_1} (T : ι → L.Theory),
  FirstOrder.Language.Theory.IsSatisfiable (⋃ i, T i) ↔
    ∀ (s : Finset ι), FirstOrder.Language.Theory.IsSatisfiable (⋃ i ∈ s, T i)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c' c'' : C} (f : c' ⟶ c'') (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c' c).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f) c)
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c'' c).inv)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_union_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).get k ⋯ = m₂.get k mem
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1
-- Lean.Meta.Basic
/-- Function parameter information cache.
 -/
Lean.Meta.ParamInfo : Type
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCriterion.Existence.stableUnderBaseChange : AlgebraicGeometry.ValuativeCriterion.Existence.IsStableUnderBaseChange
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.isContinuous_comp' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F₁ : CategoryTheory.Functor C D}
  {F₂ : CategoryTheory.Functor D E} {F₁₂ : CategoryTheory.Functor C E} (e : F₁.comp F₂ ≅ F₁₂)
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (L : CategoryTheory.GrothendieckTopology E) [F₁.IsContinuous J K] [F₂.IsContinuous K L], F₁₂.IsContinuous J L
-- Mathlib.Data.Multiset.MapFold
Multiset.map_hcongr : ∀ {α : Type u_1} {β β' : Type v} {m : Multiset α} {f : α → β} {f' : α → β'},
  β = β' → (∀ a ∈ m, f a ≍ f' a) → Multiset.map f m ≍ Multiset.map f' m
-- Mathlib.Algebra.GCDMonoid.Basic
associatesEquivOfUniqueUnits_symm_apply : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : Subsingleton αˣ] (a : α),
  associatesEquivOfUniqueUnits.symm a = Associates.mk a
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algEquivOfEq_toAlgHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hfg : f = g), ↑(AdjoinRoot.algEquivOfEq R f g hfg) = AdjoinRoot.algHomOfDvd R f g ⋯
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_sdiff_singleton_of_mem`. -/
Set.ncard_diff_singleton_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → (s \ {a}).ncard = s.ncard - 1