mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.toList_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {f : (a : α) → β a → Option (γ a)}
  {l : Std.DHashMap.Internal.AssocList α β},
  (Std.DHashMap.Internal.AssocList.filterMap f l).toList.Perm
    (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l.toList)
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.tsum_two_zpow_neg_add_one : ∑' (m : ℕ), 2 ^ (-1 - ↑m) = 1
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.instCompleteLatticeSubfunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} → CompleteLattice (CategoryTheory.Subfunctor F)
-- Init.Data.Option.Attach
_private.Init.Data.Option.Attach.0.OptionT.instMonadAttach.match_1.splitter : {m : Type u_1 → Type u_2} →
  [inst : MonadAttach m] →
    {α : Type u_1} →
      (x : OptionT m α) →
        (motive : Subtype (MonadAttach.CanReturn x.run) → Sort u_3) →
          (x_1 : Subtype (MonadAttach.CanReturn x.run)) →
            ((a : α) → (h : MonadAttach.CanReturn x.run (some a)) → motive ⟨some a, h⟩) →
              ((property : MonadAttach.CanReturn x.run none) → motive ⟨none, property⟩) → motive x_1
-- Init.Data.UInt.Lemmas
UInt8.ofNat_div : ∀ {a b : ℕ}, a < 2 ^ 8 → b < 2 ^ 8 → UInt8.ofNat (a / b) = UInt8.ofNat a / UInt8.ofNat b
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.dist_eq : ∀ {α : Type u_5} {β : Type u_6} {F : Type u_7} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x y : α),
  dist (f x) (f y) = ↑(Dilation.ratio f) * dist x y
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- `FreeSimplexQuiver.homRel` is the relation on morphisms freely generated on the
five simplicial identities.  -/
FreeSimplexQuiver.homRel : HomRel (CategoryTheory.Paths FreeSimplexQuiver)
-- Mathlib.Data.Nat.BinaryRec
Nat.bit.eq_1 : ∀ (b : Bool) (n : ℕ), Nat.bit b n = bif b then 2 * n + 1 else 2 * n
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_mul : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] (f : F) (g h : ι → M), ⇑f ∘ (g * h) = ⇑f ∘ g * ⇑f ∘ h
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.range_face_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} (s : Affine.Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1))
  {fs : Finset (Fin (n + 1))} {n' : ℕ} (h : fs.card = n' + 1),
  Set.range ((s.reindex e).face h).points = Set.range (s.face ⋯).points
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.coprime_iff_not_dvd : ∀ {p n : ℕ}, Nat.Prime p → (p.Coprime n ↔ ¬p ∣ n)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.coe_mk' : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A →ₐ[R] B)
  (h : ∀ (x : A), (↑↑f.toRingHom).toFun (star x) = star ((↑↑f.toRingHom).toFun x)),
  ⇑{ toAlgHom := f, map_star' := h } = ⇑f
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.Suggestion.processEdit : Lean.Meta.Tactic.TryThis.Suggestion → Lean.Syntax.Range → Lean.CoreM Lean.Lsp.TextEdit
-- Mathlib.Topology.QuasiSeparated
isQuasiSeparated_univ : ∀ {α : Type u_3} [inst : TopologicalSpace α] [QuasiSeparatedSpace α], IsQuasiSeparated Set.univ
-- Mathlib.Algebra.Order.Field.Basic
Mathlib.Meta.Positivity.div_ne_zero_of_ne_zero_of_pos : ∀ {α : Type u_4} [inst : GroupWithZero α] [inst_1 : PartialOrder α] {a b : α}, a ≠ 0 → 0 < b → a / b ≠ 0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedState.mk.injEq : ∀ («meta» : Lean.Meta.SavedState) («elab» : Lean.Elab.Term.State) (meta_1 : Lean.Meta.SavedState)
  (elab_1 : Lean.Elab.Term.State),
  ({ «meta» := «meta», «elab» := «elab» } = { «meta» := meta_1, «elab» := elab_1 }) =
    («meta» = meta_1 ∧ «elab» = elab_1)
-- Init.Data.BitVec.Lemmas
/-- Signed division of (x y : BitVec w) is always -2 ^ w ≤ x.toInt / y.toInt.  -/
BitVec.neg_two_pow_le_toInt_ediv : ∀ {w : ℕ} {x y : BitVec w}, -2 ^ (w - 1) ≤ x.toInt / y.toInt
-- Init.Data.Array.MapIdx
List.mapFinIdxM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (as : List α)
  (f : (i : ℕ) → α → i < as.length → m β), as.mapFinIdxM f = List.mapFinIdxM.go as f as #[] ⋯
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
isSemilinearSet_image_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {s : Set M} {F : Type u_6}
  [inst_2 : EquivLike F M N] [AddEquivClass F M N] (f : F), IsSemilinearSet (⇑f '' s) ↔ IsSemilinearSet s
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.del.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_15),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.del fvarId h) = 1 + sizeOf fvarId + sizeOf h
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
/-- The transformation matrix.  -/
Echelon.Decomposition.L : {m : Type u_1} →
  [inst : Fintype m] →
    [inst_1 : LinearOrder m] →
      {n : Type u_2} →
        [inst_2 : LinearOrder n] →
          {R : Type u_3} → [inst_3 : CommRing R] → {A : Matrix m n R} → Echelon.Decomposition A → Matrix m m R
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- If `x` satisfies Liouville condition with exponent `p` and `q < p`, then `x`
satisfies Liouville condition with exponent `q` and constant `1`.  -/
LiouvilleWith.frequently_lt_rpow_neg : ∀ {p q x : ℝ}, LiouvilleWith p x → q < p → ∃ᶠ (n : ℕ) in Filter.atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.reindex_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι')
  (i' : ι'), (b.reindex e) i' = b (e.symm i')
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.coe_coe : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : EquivLike F α β] [inst_3 : IsometryClass F α β] (f : F), ⇑↑f = ⇑f
-- Batteries.Data.UnionFind.Basic
/-- Find root of a union-find node, updating the structure using path compression.  -/
Batteries.UnionFind.find : (self : Batteries.UnionFind) → Fin self.size → (s : Batteries.UnionFind) × { _root // s.size = self.size }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α} {b : β a}, (t.insert a b).getKeyD a fallback = a
-- Init.Data.Vector.Basic
/-- `Vector α n` is an `Array α` with size `n`.  -/
Vector : Type u → ℕ → Type u
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- A semigroup homomorphism `f : M →ₙ* N` with a left-inverse `g : N → M` defines a multiplicative
equivalence between `M` and `f.srange`.

This is a bidirectional version of `MulHom.srangeRestrict`.  -/
MulEquiv.ofLeftInverse : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] → [inst_1 : Mul N] → (f : M →ₙ* N) → {g : N → M} → Function.LeftInverse g ⇑f → M ≃* ↥f.srange
-- Init.Data.Int.DivMod.Bootstrap
Int.natAbs_dvd_natAbs : ∀ {a b : ℤ}, a.natAbs ∣ b.natAbs ↔ a ∣ b
-- Mathlib.RingTheory.LocalProperties.Exactness
exact_of_localized_maximal : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid L]
  [inst_6 : Module R L] (f : M →ₗ[R] N) (g : N →ₗ[R] L),
  (∀ (J : Ideal R) [inst_7 : J.IsMaximal],
      Function.Exact ⇑((LocalizedModule.map J.primeCompl) f) ⇑((LocalizedModule.map J.primeCompl) g)) →
    Function.Exact ⇑f ⇑g
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.shiftIso_add' : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n m mn : A) (hnm : m + n = mn)
  (a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a''),
  F.shiftIso mn a a'' ⋯ =
    (F.functor a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd' D m n mn hnm) ≪≫
      ((F.functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫
        CategoryTheory.Functor.isoWhiskerRight (F.shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫
          F.shiftIso n a a' ha'
-- Mathlib.Order.RelIso.Basic
/-- Elements are related iff they are related after apply a `RelEmbedding`  -/
RelEmbedding.map_rel_iff' : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (self : r ↪r s) {a b : α},
  s (self.toEmbedding a) (self.toEmbedding b) ↔ r a b
-- Mathlib.Tactic.Linter.TextBased
Mathlib.Linter.TextBased.ErrorFormat.humanReadable.sizeOf_spec : sizeOf Mathlib.Linter.TextBased.ErrorFormat.humanReadable = 1
-- Mathlib.Analysis.Normed.Field.WithAbs
/-- If the absolute value of a normed field factors through an embedding into another normed field
that is locally compact, then the completion of the first normed field is also locally compact.  -/
AbsoluteValue.Completion.locallyCompactSpace : ∀ {K : Type u_1} [inst : Field K] {v : AbsoluteValue K ℝ} {L : Type u_2} [inst_1 : NormedField L] [CompleteSpace L]
  {f : WithAbs v →+* L} [LocallyCompactSpace L], Isometry ⇑f → LocallyCompactSpace v.Completion
-- Mathlib.Computability.Primrec.List
Primrec.listFilterMap : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → List β} {g : α → β → Option σ}, Primrec f → Primrec₂ g → Primrec fun a => List.filterMap (g a) (f a)
-- Init.Data.Array.Extract
Array.all_takeWhile : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, (Array.takeWhile p as).all p = true
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The trivial `AddSubmonoid` `{0}` of an `AddMonoid` `M`.  -/
AddSubmonoid.instBot : {M : Type u_1} → [inst : AddZeroClass M] → Bot (AddSubmonoid M)
-- Mathlib.Data.WSeq.Relation
_private.Mathlib.Data.WSeq.Relation.0.Stream'.WSeq.LiftRelO.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option (α × Stream'.WSeq α) → Option (β × Stream'.WSeq β) → Sort u_3) →
      (x : Option (α × Stream'.WSeq α)) →
        (x_1 : Option (β × Stream'.WSeq β)) →
          (Unit → motive none none) →
            ((a : α) → (s : Stream'.WSeq α) → (b : β) → (t : Stream'.WSeq β) → motive (some (a, s)) (some (b, t))) →
              ((x : Option (α × Stream'.WSeq α)) →
                  (x_2 : Option (β × Stream'.WSeq β)) →
                    (x = none → x_2 = none → False) →
                      (∀ (a : α) (s : Stream'.WSeq α) (b : β) (t : Stream'.WSeq β),
                          x = some (a, s) → x_2 = some (b, t) → False) →
                        motive x x_2) →
                motive x x_1
-- Mathlib.RingTheory.Jacobson.Ring
MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing : ∀ {n : ℕ} {R : Type u_1} [inst : CommRing R] [IsJacobsonRing R] (P : Ideal (MvPolynomial (Fin n) R)) [hP : P.IsMaximal],
  ((Ideal.Quotient.mk P).comp MvPolynomial.C).IsIntegral
-- Mathlib.Data.Sym.Basic
Sym.mem_cons_of_mem : ∀ {α : Type u_1} {n : ℕ} {s : Sym α n} {a b : α}, a ∈ s → a ∈ b ::ₛ s
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousLinearMap.continuousAt_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜] [Finite ι]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : TopologicalSpace F] [inst_5 : AddCommGroup F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜 F]
  {G : Type u_5} [inst_8 : AddCommGroup G] [inst_9 : TopologicalSpace G] [inst_10 : Module 𝕜 G]
  [inst_11 : ContinuousConstSMul 𝕜 F] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) {x : G × ((i : ι) → E i)},
  ContinuousAt (fun p => (f p.1) p.2) x
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.ReflectsLimits.reflectsCofilteredLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.im_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {f g : CategoryTheory.Arrow C} (u : f ⟶ g),
  CategoryTheory.Abelian.im.map u =
    CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π g.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι f.hom) (CategoryTheory.Arrow.Hom.right u)) ⋯
-- Init.Data.Int.Gcd
Int.gcd_mul_right_add_left : ∀ (m n k : ℤ), (k * m + n).gcd m = n.gcd m
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_X_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {k : ℕ}, (Polynomial.X ^ k).content = 1
-- Lean.Server.Requests
Lean.Server.LspResponse.mk.injEq : ∀ {α : Type} (response : α) (isComplete : Bool) (response_1 : α) (isComplete_1 : Bool),
  ({ response := response, isComplete := isComplete } = { response := response_1, isComplete := isComplete_1 }) =
    (response = response_1 ∧ isComplete = isComplete_1)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.ext_iff : ∀ {K : Type u_1} {V : Type u_2} {inst : DivisionRing K} {inst_1 : AddCommGroup V} {inst_2 : Module K V}
  {x y : Projectivization.Subspace K V}, x = y ↔ x.carrier = y.carrier
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.affineCombination_touchpointWeights : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1)))
  (i : Fin (n + 1)),
  (Finset.affineCombination ℝ Finset.univ s.points) (s.touchpointWeights signs i) = s.touchpoint signs i
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.instDistribMulActionMulOppositeAut : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] → (P : RootPairing ι R M N) → DistribMulAction P.Autᵐᵒᵖ N
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.instMonadTacticM : Monad Lean.Elab.Tactic.TacticM
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.liftAlgHom_root : ∀ {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 S R] [inst_4 : Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T)
  (h : Polynomial.eval₂ (↑i) x p = 0), (AdjoinRoot.liftAlgHom p i x h) (AdjoinRoot.root p) = x
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_sInf : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (S : Set (LieSubmodule R L M)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Analysis.Asymptotics.LinearGrowth
InfHom.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Min α] [inst_1 : Min β] (toFun toFun_1 : α → β) (e_toFun : toFun = toFun_1)
  (map_inf' : ∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b),
  { toFun := toFun, map_inf' := map_inf' } = { toFun := toFun_1, map_inf' := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], m.contains a = false → m.get! a = default
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map  -/
CategoryTheory.AddMonObj.termδ : Lean.ParserDescr
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a fallback : α},
  t.isEmpty = true → t.getD a fallback = fallback
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.finite_add : ∀ {α : Type u_2} [inst : Add α] [IsLeftCancelAdd α] [IsRightCancelAdd α] {s t : Set α},
  (s + t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCocircuit_inter_eq : ∀ {α : Type u_1} {e : α} (M : Matroid α) {B : Set α}, e ∈ B → M.fundCocircuit e B ∩ B = {e}
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepFun_const_right : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'} (X : Ω → β) (c : β'), ProbabilityTheory.CondIndepFun m' hm' X (fun x => c) μ
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The successor structure on `Arrow C ⥤ Arrow C` corresponding
to the iterations of the natural transformation
`ε : 𝟭 (Arrow C) ⟶ SmallObject.functor I.homFamily`
(see the file `SmallObject.Construction`).  -/
CategoryTheory.SmallObject.succStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [I.IsCardinalForSmallObjectArgument κ] →
              CategoryTheory.SmallObject.SuccStruct
                (CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C))
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.ofHom_hom : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (f : A ⟶ B), CommAlgCat.ofHom (CommAlgCat.Hom.hom f) = f
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd : ∀ {X Y : AlgebraicGeometry.Scheme} (U : (X ⨿ Y).Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.coprodPresheafObjIso U).hom
      CategoryTheory.Limits.prod.snd =
    AlgebraicGeometry.Scheme.Hom.app CategoryTheory.Limits.coprod.inr U
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittSub_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), (WittVector.wittSub p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian
/-- Provide `ComonObj` instances using the canonical cartesian comonoid structure.  -/
CategoryTheory.CartesianCopyDiscard.instComonObjOfCartesian : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → (X : C) → CategoryTheory.ComonObj X
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.mk.injEq : ∀ {X : SSet} {A : X.Subcomplex} (I II : Set A.N) (inter : I ∩ II = ∅) (union : I ∪ II = Set.univ) (p : ↑II ≃ ↑I)
  (I_1 II_1 : Set A.N) (inter_1 : I_1 ∩ II_1 = ∅) (union_1 : I_1 ∪ II_1 = Set.univ) (p_1 : ↑II_1 ≃ ↑I_1),
  ({ I := I, II := II, inter := inter, union := union, p := p } =
      { I := I_1, II := II_1, inter := inter_1, union := union_1, p := p_1 }) =
    (I = I_1 ∧ II = II_1 ∧ p ≍ p_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_left_strictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulRightStrictMono α] {a : α}, StrictMono fun x => x * a
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instPartialOrderFiniteIndexNormalAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  FiniteIndexNormalAddSubgroup.instPartialOrderFiniteIndexNormalAddSubgroup = inferInstance
-- Std.Sat.AIG.RelabelNat
/-- If a HashMap fulfills `Inv1` it is in an injection.
 -/
Std.Sat.AIG.RelabelNat.State.Inv1.property : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] [EquivBEq α] {n m : ℕ} (x y : α) (map : Std.HashMap α ℕ),
  Std.Sat.AIG.RelabelNat.State.Inv1 n map → map[x]? = some m → map[y]? = some m → x = y
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.revSkipWhile_bool_eq_self_iff_get : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  pos.revSkipWhile p = pos ↔ ∀ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) = false
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Delaborates the current expression as `⋯` and attaches `Elab.OmissionInfo`, which influences how the
subterm omitted by `⋯` is delaborated when hovered over.
 -/
Lean.PrettyPrinter.Delaborator.omission : Lean.PrettyPrinter.Delaborator.OmissionReason → Lean.PrettyPrinter.Delaborator.Delab
-- Lean.Meta.Tactic.LibrarySearch
/-- Create function for finding relevant declarations.
Also captures dropped entries in starLemmasExt for fallback search.  -/
Lean.Meta.LibrarySearch.libSearchFindDecls : Lean.Expr → Lean.MetaM (Array (Lean.Name × Lean.Meta.LibrarySearch.DeclMod))
-- Init.Data.List.Basic
List.length_set : ∀ {α : Type u} {as : List α} {i : ℕ} {a : α}, (as.set i a).length = as.length
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app : ∀ {X Y : SSet.Truncated 2}
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))
  (y : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso X Y).inv.app
      (SSet.Truncated.HomotopyCategory.mk x, SSet.Truncated.HomotopyCategory.mk y) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.id (X.HomotopyCategory × Y.HomotopyCategory)).obj
        (SSet.Truncated.HomotopyCategory.mk x, SSet.Truncated.HomotopyCategory.mk y))
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
subset_upperBounds_mul : ∀ {M : Type u_3} [inst : Mul M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] (s t : Set M),
  upperBounds s * upperBounds t ⊆ upperBounds (s * t)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `WithLp.equiv` as a homeomorphism.  -/
WithLp.homeomorphProd : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → WithLp p (α × β) ≃ₜ α × β
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci.sizeOf_spec : ∀ (lo : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci lo) = 1 + sizeOf lo
-- Mathlib.CategoryTheory.GuitartExact.Over
CategoryTheory.instGuitartExactOverObjOverPostOfHasBinaryProductOfPreservesLimitDiscreteWalkingPairPair : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C) [∀ (Y : C), CategoryTheory.Limits.HasBinaryProduct X Y]
  [∀ (Y : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) F],
  (CategoryTheory.TwoSquare.overPost F X).GuitartExact
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.isIso_diagonal_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f],
  CategoryTheory.IsIso (CategoryTheory.Limits.pullback.diagonal f) ↔ CategoryTheory.Mono f
-- Mathlib.Data.Set.Lattice
Set.exists_set_mem_of_union_eq_top : ∀ {β : Type u_2} {ι : Type u_12} (t : Set ι) (s : ι → Set β), ⋃ i ∈ t, s i = ⊤ → ∀ (x : β), ∃ i ∈ t, x ∈ s i
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateCont! : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.aeval_modByMonic_eq_self_of_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {p q : Polynomial R} {x : S},
  (Polynomial.aeval x) q = 0 → (Polynomial.aeval x) (p %ₘ q) = (Polynomial.aeval x) p