mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux_append_extractLsb' : ∀ {len w : ℕ} {hcast : w + (len - 1) * w = len * w} {x : BitVec (len * w)},
  0 < len →
    BitVec.addRecAux✝
        (BitVec.cast hcast (BitVec.extractLsb' ((len - 1) * w) w x ++ BitVec.extractLsb' 0 ((len - 1) * w) x)) len 0#w =
      BitVec.extractLsb' ((len - 1) * w) w x + BitVec.addRecAux✝ (BitVec.extractLsb' 0 ((len - 1) * w) x) (len - 1) 0#w
-- Mathlib.Algebra.Order.Field.Pointwise
LinearOrderedField.smul_Iic : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a r : K},
  0 < r → r • Set.Iic a = Set.Iic (r * a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The conversion from a Weierstrass curve to projective coordinates.  -/
WeierstrassCurve.toProjective : {R : Type r} → WeierstrassCurve R → WeierstrassCurve.Projective R
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Ioi_ae_eq_Ici' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a : α},
  μ {a} = 0 → Set.Ioi a =ᵐ[μ] Set.Ici a
-- Lean.Elab.InfoTree.Types
/-- Indicates that all overloaded elaborators failed. The subtrees of a `ChoiceInfo` node are the
partial `InfoTree`s of those failed elaborators. Retaining these partial `InfoTree`s helps
the language server provide interactivity even when all overloaded elaborators failed.
 -/
Lean.Elab.ChoiceInfo : Type
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.edist_inequality : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f → ∀ {x y : α}, edist x y ≠ ⊤ → edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - ↑K)
-- Init.Omega.LinearCombo
Lean.Omega.instReprLinearCombo : Repr Lean.Omega.LinearCombo
-- Mathlib.Algebra.Group.Basic
zero_sub_sub : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b : α), 0 - (a - b) = b - a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- `cfcₙ` is continuous in the variable `a : A` when `s : Set ℝ≥0` is compact and `a` varies over
nonnegative elements whose quasispectrum is contained in `s`, and the function `f` is
continuous on `s` and `f 0 = 0`.  -/
Continuous.cfcₙ_nnreal' : ∀ {X : Type u_1} {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_12 : TopologicalSpace X] {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal) {a : X → A},
      Continuous a →
        (∀ (x : X), quasispectrum NNReal (a x) ⊆ s) →
          autoParam (ContinuousOn f s) Continuous.cfcₙ_nnreal'._auto_1 →
            autoParam (f 0 = 0) Continuous.cfcₙ_nnreal'._auto_3 →
              autoParam (∀ (x : X), 0 ≤ a x) Continuous.cfcₙ_nnreal'._auto_5 → Continuous fun x => cfcₙ f (a x)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.vadd_mem : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] (p : SubAddAction R M) {x : M} (r : R), x ∈ p → r +ᵥ x ∈ p
-- Mathlib.Algebra.Opposites
MulOpposite.unop_one : ∀ {α : Type u_1} [inst : One α], MulOpposite.unop 1 = 1
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.pullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (self : CategoryTheory.Pretopology C) ⦃X Y : C⦄ (f : Y ⟶ X),
  ∀ S ∈ self.coverings X, CategoryTheory.Presieve.pullbackArrows f S ∈ self.coverings Y
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getValueCast : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] → (a : α) → (l : List ((a : α) × β a)) → Std.Internal.List.containsKey a l = true → β a
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.dest_eq_dest' : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M}
  (h : x.dest = ⟨a, f⟩) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α),
  MvPFunctor.M.dest P ⟨x, f'⟩ = MvPFunctor.M.dest' P h f'
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.dist_extend_extend : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] [inst_3 : DiscreteTopology δ] (f : α ↪ δ) (g₁ g₂ : BoundedContinuousFunction α β)
  (h₁ h₂ : BoundedContinuousFunction δ β),
  dist (BoundedContinuousFunction.extend f g₁ h₁) (BoundedContinuousFunction.extend f g₂ h₂) =
    max (dist g₁ g₂) (dist (h₁.domRestrict (Set.range ⇑f)ᶜ) (h₂.domRestrict (Set.range ⇑f)ᶜ))
-- Init.Data.SInt.Lemmas
Int64.le_iff_toInt_le : ∀ {x y : Int64}, x ≤ y ↔ x.toInt ≤ y.toInt
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.isoMk_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.MorphismProperty C}
  [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.WideSubcategory P} (e : X.obj ≅ Y.obj) (h₁ : P e.hom)
  (h₂ : P e.inv), (CategoryTheory.WideSubcategory.isoMk e h₁ h₂).hom.hom = e.hom
-- Init.Sym.Lemmas
Lean.Sym.Int32.lt_eq_false : ∀ (a b : Int32), decide (a < b) = false → (a < b) = False
-- Mathlib.Data.Set.Subset
Set.preimage_val_image_val_eq_self : ∀ {α : Type u_2} {A : Set α} {D : Set ↑A}, Subtype.val ⁻¹' Subtype.val '' D = D
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (s : Set α),
  MeasurableSet s → (∀ t ⊆ s, MeasurableSet t → v t = 0) → (∀ t ⊆ sᶜ, MeasurableSet t → w t = 0) → v.MutuallySingular w
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.toGenerators_comp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ) [inst_5 : Algebra R T]
  [inst_6 : IsScalarTower R S T], (Q.comp P).toGenerators = Q.comp P.toGenerators
-- Mathlib.Order.CompleteLattice.Defs
le_sSup_of_le : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a b : α}, b ∈ s → a ≤ b → a ≤ sSup s
-- Init.Grind.Util
Lean.Grind.nestedDecidable_congr : ∀ (p q : Prop),
  p = q → ∀ (hp : Decidable p) (hq : Decidable q), Lean.Grind.nestedDecidable hp ≍ Lean.Grind.nestedDecidable hq
-- Mathlib.Algebra.Group.ULift
ULift.addCancelMonoid : {α : Type u} → [AddCancelMonoid α] → AddCancelMonoid (ULift.{u_1, u} α)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.extend_subset : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {s t : Set ι} (hs : LinearIndepOn K v s) (hst : s ⊆ t), hs.extend hst ⊆ t
-- Init.Data.List.MinMaxIdx
List.minIdxOn_replicate : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.Refl fun x1 x2 => x1 ≤ x2] {n : ℕ} {a : α}
  {f : α → β} (h : List.replicate n a ≠ []), List.minIdxOn f (List.replicate n a) h = 0
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.ofBijective_apply_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] {n : N} (f : M →* N)
  (hf : Function.Bijective ⇑f), f ((MulEquiv.ofBijective f hf).symm n) = n
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.incl_comap : ∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}]
  {S T : (CompHausLike P)ᵒᵖ}
  (f : LocallyConstant (↑(Opposite.unop S).toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) (g : S ⟶ T)
  (a : Function.Fiber ⇑(LocallyConstant.comap (TopCat.Hom.hom g.unop.hom) f)),
  CategoryTheory.CategoryStruct.comp g
      (CompHausLike.LocallyConstant.sigmaIncl (LocallyConstant.comap (TopCat.Hom.hom g.unop.hom) f) a).op =
    CategoryTheory.CategoryStruct.comp
      (CompHausLike.LocallyConstant.sigmaIncl f
          (Function.Fiber.mk (⇑f)
            ((CategoryTheory.ConcreteCategory.hom g.unop)
              (Function.Fiber.preimage (⇑(LocallyConstant.comap (TopCat.Hom.hom g.unop.hom) f)) a)))).op
      (CompHausLike.LocallyConstant.componentHom f g.unop a).op
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The degree of a product of polynomials is equal to
the sum of the degrees.

See `Polynomial.natDegree_prod'` (with a `'`) for a version for commutative semirings,
where additionally, the product of the leading coefficients must be nonzero.
 -/
Polynomial.natDegree_prod : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R),
  (∀ i ∈ s, f i ≠ 0) → (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
-- Mathlib.Algebra.Group.ULift
ULift.rightCancelSemigroup : {α : Type u} → [RightCancelSemigroup α] → RightCancelSemigroup (ULift.{u_1, u} α)
-- Lean.Elab.Do.Basic
/-- Like `controlAt TermElabM`, but it maintains the state using the `DoElabM`'s ref cell instead of returning it
in the `TermElabM` result. This makes it possible to run multiple `DoElabM` computations in a row.
 -/
Lean.Elab.Do.controlAtTermElabM : {α : Type} →
  (({β : Type} → Lean.Elab.Do.DoElabM β → Lean.Elab.TermElabM β) → Lean.Elab.TermElabM α) → Lean.Elab.Do.DoElabM α
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal.hσ'₁ : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x)),
  (∀ (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })),
      f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op))
          (f₀ x)) →
    ∀ (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      SSet.Truncated.liftOfStrictSegal.f₂ f₀ f₁ hδ₁ hδ₀ hY
          ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.σ₂ 1 _proof_15✝ _proof_12✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.σ₂ 1 _proof_15✝ _proof_12✝).op)) (f₁ x)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.SFinite.out' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.SFinite μ],
  ∃ m, (∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (m n)) ∧ μ = MeasureTheory.Measure.sum m
-- Init.Data.Nat.Lemmas
Nat.mul_lt_mul_of_lt_of_lt : ∀ {a b c d : ℕ}, a < c → b < d → a * b < c * d
-- Mathlib.Logic.Equiv.Basic
/-- A nonempty subsingleton type is (noncomputably) equivalent to `PUnit`.  -/
Equiv.punitOfNonemptyOfSubsingleton : {α : Sort u_1} → [h : Nonempty α] → [Subsingleton α] → α ≃ PUnit.{u_9}
-- Mathlib.Logic.Denumerable
Nat.Subtype.succ.congr_simp : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s] (x x_1 : ↑s),
  x = x_1 → Nat.Subtype.succ x = Nat.Subtype.succ x_1
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isPresentable_eq_retractClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular],
  P.IsCardinalFilteredGenerator κ → CategoryTheory.isCardinalPresentable C κ = P.retractClosure
-- Mathlib.Data.Seq.Basic
Stream'.Seq.Pairwise.cons_cons_of_trans : ∀ {α : Type u} {R : α → α → Prop} [IsTrans α R] {hd tl_hd : α} {tl_tl : Stream'.Seq α},
  R hd tl_hd →
    Stream'.Seq.Pairwise R (Stream'.Seq.cons tl_hd tl_tl) →
      Stream'.Seq.Pairwise R (Stream'.Seq.cons hd (Stream'.Seq.cons tl_hd tl_tl))
-- Mathlib.Data.Finset.Pairwise
List.pairwise_iff_coe_toFinset_pairwise : ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} {l : List α} [Std.Symm r],
  l.Nodup → ((↑l.toFinset).Pairwise r ↔ List.Pairwise r l)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_ac.inj : ∀ {lhs : Bool} {s : Lean.Grind.AC.Seq} {c₁ : Lean.Meta.Grind.AC.EqCnstr} {c₂ : Lean.Meta.Grind.AC.DiseqCnstr}
  {lhs_1 : Bool} {s_1 : Lean.Grind.AC.Seq} {c₁_1 : Lean.Meta.Grind.AC.EqCnstr} {c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr},
  Lean.Meta.Grind.AC.DiseqCnstrProof.simp_ac lhs s c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_ac lhs_1 s_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Order.Cover
WCovBy.covBy_of_ne : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b → a ≠ b → a ⋖ b
-- Std.Data.HashMap.Lemmas
Std.HashMap.diff_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β}, m₁.diff m₂ = m₁ \ m₂
-- Mathlib.FieldTheory.KummerExtension
isSplittingField_AdjoinRoot_X_pow_sub_C : ∀ {K : Type u} [inst : Field K] {n : ℕ},
  (primitiveRoots n K).Nonempty →
    ∀ {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)),
      Polynomial.IsSplittingField K (AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)) (Polynomial.X ^ n - Polynomial.C a)
-- Mathlib.Order.CompleteLattice.Finset
Finset.iInf_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] (a : α) (s : α → β), ⨅ x ∈ {a}, s x = s a
-- Mathlib.Order.Hom.Basic
OrderIso.coe_trans : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (e : α ≃o β) (e' : β ≃o γ),
  ⇑(e.trans e') = ⇑e' ∘ ⇑e
-- Mathlib.Order.SuccPred.Basic
Order.Ioc_pred_left_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  ¬IsMin b → Set.Ioc (Order.pred b) a = Set.Icc b a
-- Mathlib.Computability.TuringMachine.Config
/-- Evaluating a continuation `k : Cont` on input `v : List ℕ`. This is the second part of
evaluation, when we receive results from continuations built by `stepNormal`.

* `Cont.halt v = v`, so we are done and transition to the `Cfg.halt v` state
* `Cont.cons₁ fs as k v = k (v.headI :: fs as)`, so we evaluate `fs as` now with the continuation
  `k (v.headI :: _)` (called `cons₂ v k`).
* `Cont.cons₂ ns k v = k (ns.headI :: v)`, where we now have everything we need to evaluate
  `ns.headI :: v`, so we return it to `k`.
* `Cont.comp f k v = k (f v)`, so we call `f v` with `k` as the continuation.
* `Cont.fix f k v = k (if v.headI = 0 then k v.tail else fix f v.tail)`, where `v` is a value,
  so we evaluate the if statement and either call `k` with `v.tail`, or call `fix f v` with `k` as
  the continuation (which immediately calls `f` with `Cont.fix f k` as the continuation).
 -/
Turing.ToPartrec.stepRet : Turing.ToPartrec.Cont → List ℕ → Turing.ToPartrec.Cfg
-- Mathlib.RingTheory.Ideal.Maps
/-- **Alias** of the reverse direction of `Ideal.isMaximal_map_iff_of_bijective`. -/
Ideal.IsMaximal.map_bijective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S], Function.Bijective ⇑f → ∀ {I : Ideal R}, I.IsMaximal → (Ideal.map f I).IsMaximal
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
seminormFromBounded_aux : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → ∀ (x : R), 0 ≤ c * f x
-- Std.Data.HashSet.Basic
/-- Creates a hash set from a list of elements. Note that unlike repeatedly calling `insert`, if the
collection contains multiple elements that are equal (with regard to `==`), then the last element
in the collection will be present in the returned hash set.
 -/
Std.HashSet.ofList : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → List α → Std.HashSet α
-- Batteries.Recycling.RBTree.Depth
_private.Batteries.Recycling.RBTree.Depth.0.RBTree.RBNode.depth.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (a : RBTree.RBNode α) (v : α)
  (b : RBTree.RBNode α) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b)),
  (match RBTree.RBNode.node c a v b with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c a v b => h_2 c a v b) =
    h_2 c a v b
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_ceil_singleton : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (m : ℤ),
  Int.ceil ⁻¹' {m} = Set.Ioc (↑m - 1) ↑m
-- Mathlib.Data.ZMod.Basic
/-- The **Chinese remainder theorem**. For a pair of coprime natural numbers, `m` and `n`,
  the rings `ZMod (m * n)` and `ZMod m × ZMod n` are isomorphic.

See `Ideal.quotientInfRingEquivPiQuotient` for the Chinese remainder theorem for ideals in any
ring.
 -/
ZMod.chineseRemainder : {m n : ℕ} → m.Coprime n → ZMod (m * n) ≃+* ZMod m × ZMod n
-- Mathlib.Order.SuccPred.Archimedean
strictAnti_of_succ_lt : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMax a → f (Order.succ a) < f a) → StrictAnti f
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.OrderRel.ne' : Mathlib.Meta.Positivity.OrderRel✝
-- Mathlib.GroupTheory.Transfer
MonoidHom.transfer_center_eq_pow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : (Subgroup.center G).FiniteIndex] (g : G),
  (MonoidHom.id ↥(Subgroup.center G)).transfer g = ⟨g ^ (Subgroup.center G).index, ⋯⟩
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] {f g : α →Co β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.instSubNegMonoid : {α : Type u_3} →
  [inst : UniformSpace α] → [inst_1 : AddGroup α] → [IsUniformAddGroup α] → SubNegMonoid (UniformSpace.Completion α)
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₁₃Functor_obj_obj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₃) {X Y : C₂}
  (g : X ⟶ Y) (X_1 : C₁),
  (((CategoryTheory.Functor.flip₁₃Functor.obj F).obj G).map g).app X_1 = ((F.obj X_1).map g).app G
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_inf : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → SemilatticeInf (f i)]
  [inst_2 : (i : I) → One (f i)] (i : I) (x y : f i), Pi.mulSingle i (x ⊓ y) = Pi.mulSingle i x ⊓ Pi.mulSingle i y
-- Mathlib.Algebra.GCDMonoid.Basic
StrongNormalizedGCDMonoid.toGCDMonoid : {α : Type u_2} → {inst : CommMonoidWithZero α} → [self : StrongNormalizedGCDMonoid α] → GCDMonoid α
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.continuousOn_argSelfAdjoint : ∀ {A : Type u_1} [inst : CStarAlgebra A], ContinuousOn Unitary.argSelfAdjoint (Metric.ball 1 2)
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_eq_lintegral_klFun : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  InformationTheory.klDiv μ ν =
    if μ.AbsolutelyContinuous ν then ∫⁻ (x : α), ENNReal.ofReal (InformationTheory.klFun (μ.rnDeriv ν x).toReal) ∂ν
    else ⊤
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_subset_vadd_left : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t₁ t₂ : Finset β},
  t₁ ⊆ t₂ → s +ᵥ t₁ ⊆ s +ᵥ t₂
-- Mathlib.Order.UpperLower.Closure
LowerSet.erase_eq : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {a : α}, s.erase a = s ↔ a ∉ s
-- Init.Data.SInt.Bitwise
Int16.toBitVec_abs : ∀ (a : Int16), a.abs.toBitVec = a.toBitVec.abs
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ],
  MeasureTheory.IsFiniteMeasure (μ.compProd κ)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- [Stacks Tag 00Z6](https://stacks.math.columbia.edu/tag/00Z6) -/
CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → LE (CategoryTheory.GrothendieckTopology C)
-- Mathlib.FieldTheory.Perfect
/-- A perfect ring of characteristic `p` (prime) in the sense of Serre.

NB: This is not related to the concept with the same name introduced by Bass (related to projective
covers of modules).  -/
PerfectRing : (R : Type u_1) → ℕ → [Pow R ℕ] → Prop
-- Init.Data.List.TakeDrop
List.any_dropWhile : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, ((List.dropWhile p l).any fun x => !p x) = !l.all p
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RiiSliceData.mk.injEq : ∀ {α : Type u} (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit) (range : Std.Rii α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit) (range_1 : Std.Rii α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_suffix_support_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w), q.support <:+ (p.append q).support
-- Lean.Expr
_private.Lean.Expr.0.Lean.intLEPred : Lean.Expr
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcCallParams.mk.inj : ∀ {toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams} {sessionId : UInt64} {method : Lean.Name}
  {params : Lean.Json} {toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams} {sessionId_1 : UInt64}
  {method_1 : Lean.Name} {params_1 : Lean.Json},
  { toTextDocumentPositionParams := toTextDocumentPositionParams, sessionId := sessionId, method := method,
        params := params } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1, sessionId := sessionId_1, method := method_1,
        params := params_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1 ∧
      sessionId = sessionId_1 ∧ method = method_1 ∧ params = params_1
-- Init.Data.List.Nat.TakeDrop
List.min_findIdx_findIdx : ∀ {α : Type u_1} {xs : List α} {p q : α → Bool},
  min (List.findIdx p xs) (List.findIdx q xs) = List.findIdx (fun a => p a || q a) xs
-- Mathlib.Topology.Category.Compactum
/-- A local definition used only in the proofs.  -/
_private.Mathlib.Topology.Category.Compactum.0.Compactum.cl : {X : Compactum} → Set X.A → Set X.A