mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Torsor.Basic
Prod.fst_sdiv : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : Group G] [inst_1 : Group G']
  [inst_2 : Torsor G P] [inst_3 : Torsor G' P'] (p₁ p₂ : P × P'), (p₁ /ₛ p₂).1 = p₁.1 /ₛ p₂.1
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_sigma : ∀ {α : Type u_1} {β : α → Type u_3} [inst : Fintype α] [∀ (a : α), Finite (β a)],
  Nat.card (Sigma β) = ∑ a, Nat.card (β a)
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Icc_sub : ∀ {M : Type u_4} {m n : ℕ} [inst : AddCommGroup M],
  m ≤ n → ∀ (f : ℕ → M), ∑ i ∈ Finset.Icc m n, (f (i + 1) - f i) = f (n + 1) - f m
-- Mathlib.Topology.Connected.Clopen
preconnectedSpace_iff_clopen : ∀ {α : Type u} [inst : TopologicalSpace α], PreconnectedSpace α ↔ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = Set.univ
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.all_filterM : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id m] [inst_3 : Monad m] [inst_4 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → m (ULift.{w, 0} Bool)}
  {p : β → Bool},
  Std.IterM.all p (Std.Iter.filterM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        if __do_lift.down = true then pure { down := p x } else pure { down := true })
      (Std.Iter.mapM pure it)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.equivHeightOneSpectrum_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w : NumberField.FinitePlace K),
  NumberField.FinitePlace.equivHeightOneSpectrum w = w.maximalIdeal
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_le_floor_add_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (a : R), ⌈a⌉₊ ≤ ⌊a⌋₊ + 1
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.one_lt_cof_iff : ∀ {o : Ordinal.{u_1}}, 1 < o.cof ↔ Order.IsSuccLimit o
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The `Y`-coordinate of a representative of `2 • P` for a projective point representative `P` on a
Weierstrass curve.  -/
WeierstrassCurve.Projective.dblY : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → R
-- Mathlib.Algebra.Order.Hom.Basic
/-- `AddGroupNormClass F α` states that `F` is a type of `β`-valued norms on the additive group
`α`.

You should extend this class when you extend `AddGroupNorm`.  -/
AddGroupNormClass : (F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [AddGroup α] → [AddCommMonoid β] → [PartialOrder β] → [FunLike F α β] → Prop
-- Mathlib.Algebra.Group.Action.Defs
MulAction.ext_iff : ∀ {α : Type u_9} {β : Type u_10} {inst : Monoid α} {x y : MulAction α β}, x = y ↔ SMul.smul = SMul.smul
-- Lean.ToExpr
Lean.instToExprInt64.mkNat : ℕ → Lean.Expr
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.add : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'] {l : Filter α} [ContinuousAdd ε'] {f g : α → ε'},
  MeasureTheory.IntegrableAtFilter f l μ →
    MeasureTheory.IntegrableAtFilter g l μ → MeasureTheory.IntegrableAtFilter (f + g) l μ
-- Mathlib.Order.Circular
btw_rfl_left : ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, btw a a b
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N`, we have
`f.lift hg z * g y = g x`, where `x : M, y ∈ S` are such that `z * f y = f x`.  -/
Submonoid.LocalizationMap.lift_mul_right : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N),
  (f.lift hg) z * g ↑(f.sec z).2 = g (f.sec z).1
-- Lean.Parser.Command
Lean.Parser.Command.tactic_extension.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instLeftDistribClass : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [LeftDistribClass R], LeftDistribClass (Lex R)
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentRegistrationOptions.documentSelector? : Lean.Lsp.TextDocumentRegistrationOptions → Option Lean.Lsp.DocumentSelector
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The type of good products is equivalent to its image.  -/
Profinite.NobelingProof.GoodProducts.equiv_range : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] → ↑(Profinite.NobelingProof.GoodProducts C) ≃ ↑(Profinite.NobelingProof.GoodProducts.range C)
-- Mathlib.Algebra.Order.Group.Defs
le_inv_self_iff : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {a : α}, a ≤ a⁻¹ ↔ a ≤ 1
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.mrange_eq_iSup : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_4} [inst_1 : Monoid N]
  (f : (i : ι) → M i →* N), MonoidHom.mrange (Monoid.CoprodI.lift f) = ⨆ i, MonoidHom.mrange (f i)
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
Metric.inseparable_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, Inseparable x y ↔ dist x y = 0
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.map_map : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} {E : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : CommRing R]
  [inst_6 : TopologicalSpace R] [inst_7 : IsTopologicalRing R] [inst_8 : Module R E] [inst_9 : ContinuousSMul R E]
  {Z : Type u_5} [inst_10 : TopologicalSpace Z] (f : C(X, Y)) (g : C(Y, Z)) (μ : AbstractMeasure X R E),
  (AbstractMeasure.map g) ((AbstractMeasure.map f) μ) = (AbstractMeasure.map (g.comp f)) μ
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.comm_tmul : ∀ (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 : A) (b : B),
  (Algebra.TensorProduct.comm R A B) (a ⊗ₜ[R] b) = b ⊗ₜ[R] a
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- A cone `t` over `F` is a weak limit cone if each cone over `F` admits a
cone morphism to `t`.  -/
CategoryTheory.Limits.IsWeakLimit : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cone F → Type (max (max u_1 u_3) v_3)
-- Mathlib.Combinatorics.SimpleGraph.Paths
_private.Mathlib.Combinatorics.SimpleGraph.Paths.0.SimpleGraph.Walk.bypass.match_1.splitter : {V : Type u_1} →
  {G : SimpleGraph V} →
    {u : V} →
      (motive : (v : V) → G.Walk u v → Sort u_2) →
        (v : V) →
          (x : G.Walk u v) →
            (Unit → motive u SimpleGraph.Walk.nil) →
              ((v v_1 : V) → (ha : G.Adj u v_1) → (p : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons ha p)) →
                motive v x
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {len : ℕ} →
        (aig : Std.Sat.AIG α) →
          (idx : ℕ) →
            idx ≤ len →
              aig.RefVec idx →
                aig.RefVec len →
                  (f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α) →
                    [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] →
                      [Std.Sat.AIG.RefVec.LawfulMapOperator α f] → Std.Sat.AIG.RefVecEntry α len
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Fintype.prod_ite_eq_ite_exists : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Fintype ι] (p : ι → Prop) [inst_2 : DecidablePred p],
  (∀ (i j : ι), p i → p j → i = j) → ∀ (a : M), (∏ i, if p i then a else 1) = if ∃ i, p i then a else 1
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
/-- If `#ErdosStone.filter` is sufficiently large, then there exist a `y` such that there
are least `t` vertices in the fiber `ErdosStone.filter.pi A · = y`.

This is an auxiliary theorem for the Erdős-Stone theorem.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.filter.pi.exists_le_card_fiber : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj] {ε : ℝ} {r t t' : ℕ}
  (K : G.CompleteEquipartiteSubgraph r t'),
  0 < r →
    0 < t' →
      t < t' →
        ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n →
          (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t) →
            ∃ y, t ≤ {w | SimpleGraph.ErdosStone.filter.pi✝ K w = y}.card
-- Mathlib.Algebra.Group.End
Equiv.Perm.coe_mul : ∀ {α : Type u_4} (f g : Equiv.Perm α), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.leadingCoeff_hermite : ∀ (n : ℕ), (Polynomial.hermite n).leadingCoeff = 1
-- Mathlib.Order.WithBot
/-- The order on `WithBot α`, defined by `⊥ ≤ y` and `a ≤ b → ↑a ≤ ↑b`.

Equivalently, `x ≤ y` can be defined as `∀ a : α, x = ↑a → ∃ b : α, y = ↑b ∧ a ≤ b`,
see `le_iff_forall`. The definition as an inductive predicate is preferred since it
cannot be accidentally unfolded too far.  -/
WithBot.instLE : {α : Type u_1} → [LE α] → LE (WithBot α)
-- Lean.Server.FileWorker.SemanticHighlighting
/-- The state used to handle computing non-overlapping semantic tokens. See
`handleOverlappingSemanticTokens` for a description of the problem.

Tokens are computed by iterating over every token _boundary_. At a given boundary, one of the
following things may happen:
1. We leave the range of a token, and there is no current token
2. We leave the range of a token, starting a new one
3. We start a token when there was none before

To do this, we maintain a set of tokens that could in principle occupy the interval from the last
token boundary to the one being considered. This includes tokens that are already in progress, and
potentially a new one from the input. The one with the highest priority is selected to be the next
one at each transition.
 -/
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState : Type
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.Std.Slice.Internal.ByteSliceData.mk.inj : ∀ {byteArray : ByteArray} {start stop : ℕ} {start_le_stop : start ≤ stop}
  {stop_le_size_byteArray : stop ≤ byteArray.size} {byteArray_1 : ByteArray} {start_1 stop_1 : ℕ}
  {start_le_stop_1 : start_1 ≤ stop_1} {stop_le_size_byteArray_1 : stop_1 ≤ byteArray_1.size},
  { byteArray := byteArray, start := start, stop := stop, start_le_stop := start_le_stop,
        stop_le_size_byteArray := stop_le_size_byteArray } =
      { byteArray := byteArray_1, start := start_1, stop := stop_1, start_le_stop := start_le_stop_1,
        stop_le_size_byteArray := stop_le_size_byteArray_1 } →
    byteArray = byteArray_1 ∧ start = start_1 ∧ stop = stop_1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.IsModHom.mulActionHom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] {Y : C}
  [inst_4 : CategoryTheory.ModObj M Y] (f : X ⟶ Y) [inst_5 : CategoryTheory.IsModHom M f] (Z : C),
  CategoryTheory.IsModHom.mulActionHom f Z =
    { toFun := fun x => CategoryTheory.CategoryStruct.comp x f, map_smul' := ⋯ }
-- Mathlib.Data.Ordmap.Invariants
Ordnode.all_node' : ∀ {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α},
  Ordnode.All P (l.node' x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r
-- Mathlib.Order.OrdContinuous
/-- Convert an injective left order continuous function to an order embedding.  -/
LeftOrdContinuous.toOrderEmbedding : {α : Type u} →
  {β : Type v} →
    [inst : SemilatticeSup α] →
      [inst_1 : SemilatticeSup β] → (f : α → β) → LeftOrdContinuous f → Function.Injective f → α ↪o β
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.lift.eq_1 : ∀ {V : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ : CategoryTheory.Functor J C}
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  (s : CategoryTheory.Limits.Cone (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)),
  CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.lift s =
    CategoryTheory.Limits.end_.lift
      (fun j =>
        CategoryTheory.CategoryStruct.comp (s.π.app j)
          (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V ((CategoryTheory.Under.forget j).comp F₁)
            ((CategoryTheory.Under.forget j).comp F₂) (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id j))))
      ⋯
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.naturality_associator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {p f g h pf pfg pfgh : C} (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
  (η_g : CategoryTheory.MonoidalCategoryStruct.tensorObj pf g ≅ pfg)
  (η_h : CategoryTheory.MonoidalCategoryStruct.tensorObj pfg h ≅ pfgh),
  CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategoryStruct.associator f g h) ≪≫
      Mathlib.Tactic.Monoidal.normalizeIsoComp η_f (Mathlib.Tactic.Monoidal.normalizeIsoComp η_g η_h) =
    Mathlib.Tactic.Monoidal.normalizeIsoComp (Mathlib.Tactic.Monoidal.normalizeIsoComp η_f η_g) η_h
-- Init.Data.SInt.Lemmas
Int16.lt_iff_le_and_ne : ∀ {a b : Int16}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Index of a bump function such that `fs i =ᶠ[𝓝 x] 1`.  -/
SmoothBumpCovering.ind : {ι : Type uι} →
  {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] →
                    [inst_5 : FiniteDimensional ℝ E] → {s : Set M} → SmoothBumpCovering ι I M s → (x : M) → x ∈ s → ι
-- Init.Data.Array.Attach
Array.filter_wfParam : ∀ {α : Type u_1} {xs : Array α} {f : α → Bool}, Array.filter f (wfParam xs) = Array.filter f xs.attach.unattach
-- Mathlib.SetTheory.Ordinal.Family
/-- `le_ciSup` whenever the input type is small in the output universe. This lemma sometimes
fails to infer `f` in simple cases and needs it to be given explicitly.  -/
Ordinal.le_iSup : ∀ {ι : Type u_3} (f : ι → Ordinal.{u}) [Small.{u, u_3} ι] (i : ι), f i ≤ ⨆ i, f i
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- A BigOperator binder in parentheses  -/
BigOperators.bigOpBinderParenthesized : Lean.ParserDescr
-- Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
AddChar.card_addChar_le : ∀ (G : Type u_1) (R : Type u_3) [inst : AddCommGroup G] [inst_1 : RCLike R] [inst_2 : Fintype G],
  Fintype.card (AddChar G R) ≤ Fintype.card G
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_negSucc : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (n : ℕ), ↑(-(↑n + 1)) = -(↑n + 1)
-- Mathlib.Order.WellFoundedSet
Set.isWF_empty : ∀ {α : Type u_2} [inst : LT α], ∅.IsWF
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_add_int : ∀ (f : CircleDeg1Lift) (x : ℝ) (m : ℤ), f (x + ↑m) = f x + ↑m
-- Mathlib.Analysis.Distribution.FourierMultiplier
SchwartzMap.lineDeriv_eq_fourierMultiplierCLM : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] [CompleteSpace F] (m : E) (f : SchwartzMap E F),
  LineDeriv.lineDerivOp m f = (2 * ↑Real.pi * Complex.I) • (SchwartzMap.fourierMultiplierCLM F fun x => inner ℝ x m) f
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.ExtDTreeMap.Const.maxEntryD : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α × β → α × β
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `J(a | n) = -1`, then `n` has a prime divisor `p` such that `J(a | p) = -1`.  -/
jacobiSym.eq_neg_one_at_prime_divisor_of_eq_neg_one : ∀ {a : ℤ} {n : ℕ}, jacobiSym a n = -1 → ∃ p, Nat.Prime p ∧ p ∣ n ∧ jacobiSym a p = -1
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanIdentifier.mk.inj : ∀ {module decl : Lean.Name} {isExactMatch : Bool} {module_1 decl_1 : Lean.Name} {isExactMatch_1 : Bool},
  { module := module, decl := decl, isExactMatch := isExactMatch } =
      { module := module_1, decl := decl_1, isExactMatch := isExactMatch_1 } →
    module = module_1 ∧ decl = decl_1 ∧ isExactMatch = isExactMatch_1
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_neg_of_neg_of_pos : ∀ {a b : ℤ}, a < 0 → 0 < b → a.fdiv b < 0
-- Mathlib.Logic.Function.Basic
/-- On non-dependent functions, `Function.update` can be expressed as an `ite`  -/
Function.update_apply : ∀ {α : Sort u} [inst : DecidableEq α] {β : Sort u_1} (f : α → β) (a' : α) (b : β) (a : α),
  Function.update f a' b a = if a = a' then b else f a
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app._auto_1) {Z : C}
  (h : (CategoryTheory.unopUnop C).obj ((CategoryTheory.shiftFunctor Cᵒᵖᵒᵖ n).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (CategoryTheory.unopUnop C) n).inv.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app (Opposite.unop X)).unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app X).unop.unop h)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_minKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → t.minKey?.isSome = true
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.modify.congr_simp : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] [inst_2 : Hashable α] {β : Type v}
  (m m_1 : Std.DHashMap.Raw α fun x => β),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (f f_1 : β → β), f = f_1 → Std.DHashMap.Raw.Const.modify m a f = Std.DHashMap.Raw.Const.modify m_1 a_1 f_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α}
  {v : β},
  t.WF →
    ((k, v) ∈ Std.DTreeMap.Internal.Impl.Const.toList t ↔
      t.getKey? k = some k ∧ Std.DTreeMap.Internal.Impl.Const.get? t k = some v)
-- Qq.MatchImpl
Qq.Impl.mkLambda' : Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.Partition.colorable : ∀ {V : Type u} {G : SimpleGraph V} (P : G.Partition) [inst : Fintype ↑P.parts], G.Colorable (Fintype.card ↑P.parts)
-- Mathlib.Data.PNat.Xgcd
PNat.gcd_rel_right' : ∀ (a b : ℕ+), a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instCategory : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] → [inst_2 : Monoid G] → CategoryTheory.Category.{w, max (max (w + 1) v) u} (TopRep k G)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k fallback : α}, m₂.contains k = false → (m₁.inter m₂).getKeyD k fallback = fallback
-- Mathlib.RingTheory.PiTensorProduct
/-- To show two algebra morphisms from finite tensor products are equal, it suffices to show that
they agree on elements of the form $1 ⊗ ⋯ ⊗ a ⊗ 1 ⊗ ⋯$.  -/
PiTensorProduct.algHom_ext : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {S : Type u_5} [Finite ι] [inst_4 : DecidableEq ι] [inst_5 : Semiring S]
  [inst_6 : Algebra R S] ⦃f g : (PiTensorProduct R fun i => A i) →ₐ[R] S⦄,
  (∀ (i : ι), f.comp (PiTensorProduct.singleAlgHom i) = g.comp (PiTensorProduct.singleAlgHom i)) → f = g
-- Std.Data.DTreeMap.Internal.Operations
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getThenInsertIfNew? : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.LawfulEqOrd α] →
        (t : Std.DTreeMap.Internal.Impl α β) →
          (k : α) → β k → t.Balanced → Option (β k) × Std.DTreeMap.Internal.Impl α β
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {w n : ℕ} {lhs : aig.RefVec w}
  {rhs : aig.RefVec n} {pow n_1 : ℕ} {lhs_1 : aig.RefVec w} {rhs_1 : aig.RefVec n_1} {pow_1 : ℕ},
  { n := n, lhs := lhs, rhs := rhs, pow := pow } = { n := n_1, lhs := lhs_1, rhs := rhs_1, pow := pow_1 } →
    n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1 ∧ pow = pow_1
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_finCongr_Ico : ∀ {n m : ℕ} (h : n = m) (i j : Fin n),
  Finset.map (finCongr h).toEmbedding (Finset.Ico i j) = Finset.Ico (Fin.cast h i) (Fin.cast h j)
-- Init.Data.Order.Opposite
LE.le_opposite_iff : ∀ {α : Type u_1} {le : LE α} {a b : α}, a ≤ b ↔ b ≤ a
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Hom.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Pseudofunctor.StrongTrans.Hom η θ},
  x.as = y.as → x = y
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.card_neighborSet_union_compl_neighborSet : ∀ {V : Type u} [inst : Fintype V] (G : SimpleGraph V) (v : V) [inst_1 : Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)],
  (G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset.card = Fintype.card V - 1
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- `LinearMap.lTensor M f : M ⊗ N →ₗ M ⊗ P` is the natural linear map
induced by `f : N →ₗ P`.  -/
LinearMap.lTensor : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      {N : Type u_8} →
        {P : Type u_9} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] → (N →ₗ[R] P) → TensorProduct R M N →ₗ[R] TensorProduct R M P
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- This is the `norm_num` plug-in that evaluates Jacobi symbols.  -/
Tactic.NormNum.evalJacobiSym : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
/-- membership in a FactorSet (bundled version)  -/
Associates.BfactorSetMem : {α : Type u_1} → [inst : CommMonoidWithZero α] → { a // Irreducible a } → Associates.FactorSet α → Prop