mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.ι_π_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C) {Z : C} (h : Φ.quotient.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.ι.app X) (CategoryTheory.CategoryStruct.comp (Φ.π.app X) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {fallback : β} {f : Option β → Option β},
  (t.alter k f).getD k' fallback = if cmp k k' = Ordering.eq then (f t[k]?).getD fallback else t.getD k' fallback
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
/-- Any entry of any member of `l.ranges` is strictly smaller than `l.sum`.  -/
List.mem_mem_ranges_iff_lt_sum : ∀ (l : List ℕ) {n : ℕ}, (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_add : ∀ {α : Type u_1} [inst : Add α] (a b : αᵒᵈ), OrderDual.ofDual (a + b) = OrderDual.ofDual a + OrderDual.ofDual b
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.inf_basis_neBot_iff : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  l.HasBasis p s → l'.HasBasis p' s' → ((l ⊓ l').NeBot ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → (s i ∩ s' i').Nonempty)
-- Mathlib.Analysis.Fourier.AddCircle
AddCircle.haarAddCircle.congr_simp : ∀ {T : ℝ} [hT : Fact (0 < T)], AddCircle.haarAddCircle = AddCircle.haarAddCircle
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The identity based functor.  -/
CategoryTheory.BasedFunctor.id : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] → (𝒳 : CategoryTheory.BasedCategory 𝒮) → CategoryTheory.BasedFunctor 𝒳 𝒳
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = true → t.minKey! = default
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalTermRingMode : Lean.Elab.ConfigEval.EvalTerm Mathlib.Tactic.RingNF.RingMode
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_swap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ],
  MeasureTheory.Measure.map Prod.swap (μ.prod ν) = ν.prod μ
-- Std.Http.Data.Status
/-- 416 Range Not Satisfiable
 -/
Std.Http.Status.rangeNotSatisfiable : Std.Http.Status
-- Lean.Elab.Binders
/-- If `binder` is a `_` or an identifier, return a `bracketedBinder` using `type` otherwise throw an exception.  -/
Lean.Elab.Term.expandSimpleBinderWithType : Lean.Term → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_iso_pushout : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.CommSq f g inl inr →
    ∀ [inst_1 : CategoryTheory.Limits.HasPushout f g] (i : P ≅ CategoryTheory.Limits.pushout f g),
      CategoryTheory.CategoryStruct.comp inl i.hom = CategoryTheory.Limits.pushout.inl f g →
        CategoryTheory.CategoryStruct.comp inr i.hom = CategoryTheory.Limits.pushout.inr f g →
          CategoryTheory.IsPushout f g inl inr
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_domRestrict : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M),
  (f.domRestrict K).ker = f.ker.subgroupOf K
-- Mathlib.Data.Int.ModEq
Int.modEq_mul_modulus_add_iff : ∀ {n a b c : ℤ}, a ≡ b * n + c [ZMOD n] ↔ a ≡ c [ZMOD n]
-- Mathlib.Data.TypeVec
TypeVec.toSubtype'.eq_def : ∀ {n : ℕ} {α : TypeVec.{u} n} (p : (α.prod α).Arrow (TypeVec.repeat n Prop)) (x : Fin2 n)
  (x_1 : { x_1 // TypeVec.ofRepeat (p x (TypeVec.prod.mk x x_1.1 x_1.2)) }),
  TypeVec.toSubtype' p x x_1 =
    match n, α, p, x, x_1 with
    | .(n + 1), α, p, i.fs, x => TypeVec.toSubtype' (TypeVec.dropFun p) i x
    | .(n + 1), α, p, Fin2.fz, x => ⟨↑x, ⋯⟩
-- Mathlib.CategoryTheory.GradedObject.Single
CategoryTheory.GradedObject.singleObjApplyIsoOfEq_inv_single_map : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) (i : J)
  (h : i = j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h).inv
      ((CategoryTheory.GradedObject.single j).map f i) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j Y i h).inv
-- Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
/-- **Alias** of `MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty`.

---

The `G`-action on `X` is proper iff, for each pair of compacts `U, V` in `X`,
the set of `g` such that `U` intersects `g • V` is compact.

See `ProperSMul.isCompact_setOfPred_inter_nonempty`
for a one-way implication with fewer conditions.

**Note**: We assume `CompactlyCoherentSpace (X × X)`
as this is the minimal assumption needed to make the proof work;
but this follows from various more familiar conditions,
such as `FirstCountableTopology X`.
Importing `Mathlib.Topology.Sequences` makes this implication available.
 -/
MulAction.properSMul_iff_isCompact_setOf_inter_nonempty : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  [inst_3 : MulAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [ContinuousSMul G X],
  ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitToOpenPartialHomeomorph_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤),
  ↑(HasStrictFDerivAt.implicitToOpenPartialHomeomorph f f' hf hf') a = (f a, 0)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_coeSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (G'' : G'.coe.Subgraph),
  (SimpleGraph.Subgraph.coeSubgraph G'').verts = Subtype.val '' G''.verts
-- Lean.ExtraModUses
Lean.IndirectModUse : Type
-- Mathlib.Analysis.Fourier.AddCircle
/-- Haar measure on the additive circle, normalised to have total measure 1.  -/
AddCircle.haarAddCircle : {T : ℝ} → [hT : Fact (0 < T)] → MeasureTheory.Measure (AddCircle T)
-- Mathlib.Analysis.InnerProductSpace.MulOpposite
MulOpposite.inner_unop : ∀ {𝕜 : Type u_1} {H : Type u_2} [inst : Inner 𝕜 H] (x y : Hᵐᵒᵖ),
  inner 𝕜 (MulOpposite.unop x) (MulOpposite.unop y) = inner 𝕜 x y
-- Mathlib.GroupTheory.GroupAction.Period
MulAction.period_dvd_exponent : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] (m : M) (a : α),
  MulAction.period m a ∣ Monoid.exponent M
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unsafeForwardRule.inj : ∀ {r₁ : Aesop.ForwardRule} {r₂ : Aesop.UnsafeRule} {r₁_1 : Aesop.ForwardRule} {r₂_1 : Aesop.UnsafeRule},
  Aesop.BaseRuleSetMember.unsafeForwardRule r₁ r₂ = Aesop.BaseRuleSetMember.unsafeForwardRule r₁_1 r₂_1 →
    r₁ = r₁_1 ∧ r₂ = r₂_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.equiv_emptyWithCapacity_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {c : ℕ}, m.Equiv (Std.DHashMap.emptyWithCapacity c) ↔ m.isEmpty = true
-- Mathlib.Order.WithBot
/-- Function that sends an element of `WithTop α` to `α`,
with an arbitrary default value for `⊤`.  -/
WithTop.untopA : {α : Type u_1} → [Nonempty α] → WithTop α → α
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.map_map_homMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (φ : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.FreeGroupoid.map φ).map (CategoryTheory.FreeGroupoid.homMk f) =
    CategoryTheory.FreeGroupoid.homMk (φ.map f)
-- Lean.Data.Json.Basic
Lean.Json.instCoeRawStringStructured : Coe (Std.TreeMap.Raw String Lean.Json compare) Lean.Json.Structured
-- Mathlib.NumberTheory.FermatPsp
/-- Used in the proof of `psp_from_prime_psp`
 -/
_private.Mathlib.NumberTheory.FermatPsp.0.Nat.bp_helper : ∀ {b p : ℕ}, 0 < b → 1 ≤ p → b ^ (2 * p) - 1 - (b ^ 2 - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right_cert.eq_1 : ∀ (p₁ p₂ : Int.Internal.Linear.Poly) (n : ℕ),
  Int.Internal.Linear.cooper_right_cert p₁ p₂ n =
    Int.Internal.Linear.Poly.casesOn p₁ (fun x => false) fun a x x_1 =>
      Int.Internal.Linear.Poly.casesOn p₂ (fun x => false) fun b y x_2 =>
        (Nat.beq x y).and' ((decide (a < 0)).and' ((decide (b > 0)).and' (n.beq b.natAbs)))
-- Lean.MetavarContext
Lean.DelayedMetavarAssignment.fvarsExp : Lean.DelayedMetavarAssignment → Array Lean.Expr
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.isEmbedding_inducingFn : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] [SeparatingDual 𝕜₂ F],
  Topology.IsEmbedding ⇑(ContinuousLinearMapWOT.inducingFn σ E F)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.MonadInfo.mk.inj : ∀ {m : Lean.Expr} {u v : Lean.Level} {cachedPUnit cachedPUnitUnit m_1 : Lean.Expr} {u_1 v_1 : Lean.Level}
  {cachedPUnit_1 cachedPUnitUnit_1 : Lean.Expr},
  { m := m, u := u, v := v, cachedPUnit := cachedPUnit, cachedPUnitUnit := cachedPUnitUnit } =
      { m := m_1, u := u_1, v := v_1, cachedPUnit := cachedPUnit_1, cachedPUnitUnit := cachedPUnitUnit_1 } →
    m = m_1 ∧ u = u_1 ∧ v = v_1 ∧ cachedPUnit = cachedPUnit_1 ∧ cachedPUnitUnit = cachedPUnitUnit_1
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_eq_of_notMem : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)] {i : ι},
  i ∉ s → s.piecewise f g i = g i
-- Init.Core
imp_iff_not : ∀ {a b : Prop}, ¬b → (a → b ↔ ¬a)
-- Mathlib.Order.Ideal
Order.Ideal.ext : ∀ {P : Type u_1} [inst : LE P] {s t : Order.Ideal P}, ↑s = ↑t → s = t
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
SSet.Subcomplex.BicartSq.isPushout : ∀ {X : SSet} {A₁ A₂ A₃ A₄ : X.Subcomplex} (sq : A₁.BicartSq A₂ A₃ A₄),
  CategoryTheory.IsPushout (SSet.Subcomplex.homOfLE ⋯) (SSet.Subcomplex.homOfLE ⋯) (SSet.Subcomplex.homOfLE ⋯)
    (SSet.Subcomplex.homOfLE ⋯)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sInf_of_not_bddBelow : ∀ {s : Set ℝ}, ¬BddBelow s → sInf s = 0
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_target'' : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  (e.trans e').target = ↑e' '' (e'.source ∩ e.target)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l → k ∈ List.map Sigma.fst l → (m.insertMany l).getKey! k' = k
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr : Type
-- Mathlib.CategoryTheory.Sites.Closed
CategoryTheory.Functor.sieves_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : Cᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.Functor.sieves C).map f = TypeCat.ofHom fun S => CategoryTheory.Sieve.pullback f.unop S
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.fac_right_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : X ⟶ A} {i : B ⟶ A} {p : Y ⟶ X}
  {g : Y ⟶ B} (sq : CategoryTheory.CommSq g p i f) [hsq : sq.HasLift] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp sq.lift (CategoryTheory.CategoryStruct.comp i h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.op_distinguished : ∀ {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.distinguishedTriangles,
    (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f` is an immersion at `x` and `g = f` on some neighbourhood of `x`,
then `g` is an immersion at `x`.  -/
Manifold.IsImmersionAtOfComplement.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M},
  Manifold.IsImmersionAtOfComplement F I J n f x → f =ᶠ[nhds x] g → Manifold.IsImmersionAtOfComplement F I J n g x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.equivII_apply_coe : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (a : h.ι), ↑(h.equivII a) = h.type₂ a
-- Init.Prelude
/-- Gets the number of arguments of the syntax node, or `0` if it's not a `node`.  -/
Lean.Syntax.getNumArgs : Lean.Syntax → ℕ
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_mul_succ_div : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → a < b * Order.succ (a / b)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.minEntry : {α : Type u} → {β : α → Type v} → (t : Std.DTreeMap.Internal.Impl α β) → t.isEmpty = false → (a : α) × β a
-- Init.Prelude
/-- If `ref? = some ref`, run `x : m α` with a modified value for the `ref` by calling `withRef`.
Otherwise, run `x` directly.
 -/
Lean.withRef? : {m : Type → Type} → [Monad m] → [Lean.MonadRef m] → {α : Type} → Option Lean.Syntax → m α → m α
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddAction.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α],
  Shrink.instAddAction = Equiv.addAction M (equivShrink α).symm
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- The precomposition on the types `SmallShiftedHom W` with a morphism
which satisfies `W` is a bijection.  -/
CategoryTheory.Localization.SmallShiftedHom.precompEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {M : Type w'} →
        [inst_1 : AddMonoid M] →
          [inst_2 : CategoryTheory.HasShift C M] →
            {X Y Z : C} →
              [W.RespectsIso] →
                [W.IsCompatibleWithShift M] →
                  [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X X] →
                    [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y] →
                      [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] →
                        [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y X] →
                          [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z] →
                            [inst_10 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z] →
                              [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] →
                                (f : X ⟶ Y) →
                                  W f →
                                    {a : M} →
                                      CategoryTheory.Localization.SmallShiftedHom W Y Z a ≃
                                        CategoryTheory.Localization.SmallShiftedHom W X Z a
-- Mathlib.Combinatorics.Colex
/-- The colexicographic order is insensitive to removing the same elements from both sets.  -/
Finset.Colex.toColex_sdiff_le_toColex_sdiff : ∀ {α : Type u_1} [inst : PartialOrder α] {s t u : Finset α} [inst_1 : DecidableEq α],
  u ⊆ s → u ⊆ t → (toColex (s \ u) ≤ toColex (t \ u) ↔ toColex s ≤ toColex t)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Mon C)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.eq_bot_of_card_le : ∀ {M : Type u_1} [inst : Monoid M] {S : Submonoid M} [inst_1 : Fintype ↥S], Fintype.card ↥S ≤ 1 → S = ⊥
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toArray_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {f : α → β → Bool},
  t.WF →
    Std.DTreeMap.Internal.Impl.Const.toArray (Std.DTreeMap.Internal.Impl.filter! f t) =
      Array.filter (fun p => f p.1 p.2) (Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α},
  (List.map Prod.fst l).contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey? k = none
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If there is any isomorphism `G.obj ⊤ ⟶ ⊤`, then `G` preserves terminal objects.  -/
CategoryTheory.Limits.preservesTerminal_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasTerminal D] (f : G.obj (⊤_ C) ⟶ ⊤_ D) [i : CategoryTheory.IsIso f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.omega_mul_omega_eq_algebraMap : ∀ {R : Type u_2} {a b : R} [inst : CommSemiring R],
  QuadraticAlgebra.omega * QuadraticAlgebra.omega =
    (algebraMap R (QuadraticAlgebra R a b)) a + (algebraMap R (QuadraticAlgebra R a b)) b * QuadraticAlgebra.omega
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.one_mul : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → NonAssocSemiring (A i)]
  [inst_2 : (i : ι) → Module R (A i)] [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)]
  [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)] (x : PiTensorProduct R fun i => A i),
  (PiTensorProduct.mul ((PiTensorProduct.tprod R) 1)) x = x
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Topology.IsClosedEmbedding.measurableEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [mα : MeasurableSpace α] [BorelSpace α]
  [mβ : TopologicalSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β] {f : α → β},
  Topology.IsClosedEmbedding f → MeasurableEmbedding f
-- Mathlib.Order.Basic
update_lt_self_iff : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x : (i : ι) → π i}
  {i : ι} {a : π i}, Function.update x i a < x ↔ a < x i
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.isEmpty_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  [LawfulMonad m] [Std.Iterators.Productive α m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.isEmpty = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it out => pure { down := false }
      | Std.IterStep.skip it' => it'.isEmpty
      | Std.IterStep.done => pure { down := true }
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_le_of_le_div' : ∀ {a b c : ENNReal}, a ≤ b / c → c * a ≤ b
-- Mathlib.Order.Filter.Partial
Filter.rcomap_rcomap : ∀ {α : Type u} {β : Type v} {γ : Type w} (r : SetRel α β) (s : SetRel β γ) (l : Filter γ),
  Filter.rcomap r (Filter.rcomap s l) = Filter.rcomap (r.comp s) l
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
/-- Although not explicitly stated, the assumptions of lemma `natDegree_C_mul_of_mul_ne_zero`
force the polynomial `p` to be non-zero, via `p.leadingCoeff ≠ 0`.
 -/
Polynomial.natDegree_C_mul_of_mul_ne_zero : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R},
  a * p.leadingCoeff ≠ 0 → (Polynomial.C a * p).natDegree = p.natDegree
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.toSimpleGraph_adj : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C) (hv : v ∈ C),
  C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨v, hv⟩ ↔ G.Adj u v
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.nonempty_sup_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) [Q.Nonempty],
  (P ⊔ Q).Nonempty
-- Init.Data.SInt.Basic
/-- Bitwise complement, also known as bitwise negation, for 16-bit signed integers. Usually accessed via
the `~~~` prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.
Integers use the two's complement representation, so `Int16.complement a = -(a + 1)`.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.complement : Int16 → Int16
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)},
      List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
        (∀ a ∈ t, (List.map Sigma.fst l).contains a = false) → (t.insertMany l).size = t.size + l.length
-- Mathlib.Tactic.DepRewrite
/-- Embedding of `CastMode` into naturals.  -/
Mathlib.Tactic.DepRewrite.CastMode.toNat : Mathlib.Tactic.DepRewrite.CastMode → ℕ
-- Mathlib.Algebra.Ring.Ext
NonUnitalRing.toNonUnitalNonAssocring_injective : ∀ {R : Type u}, Function.Injective (@NonUnitalRing.toNonUnitalNonAssocRing R)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.adicAbv_add_le_max`.

---

The `v`-adic absolute value satisfies the ultrametric inequality.  -/
NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x y : K),
  (NumberField.HeightOneSpectrum.adicAbv K v) (x + y) ≤
    max ((NumberField.HeightOneSpectrum.adicAbv K v) x) ((NumberField.HeightOneSpectrum.adicAbv K v) y)