mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoendFunctor_map : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C]
  {X Y : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (f : X ⟶ Y),
  CategoryTheory.Limits.chosenCoendFunctor.map f = CategoryTheory.Limits.chosenCoend.map f
-- Mathlib.Algebra.Order.Module.Defs
SMulPosStrictMono.toSMulPosMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : PartialOrder α]
  [inst_4 : PartialOrder β] [SMulPosStrictMono α β], SMulPosMono α β
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- If `f` only depends on variables up to rank `b`, its integral from `a` to `b` only depends on
variables up to rank `a`.  -/
DependsOn.dependsOn_lmarginalPartialTraj : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {b : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsSFiniteKernel (κ n)] (a : ℕ) {f : ((n : ℕ) → X n) → ENNReal},
  DependsOn f ↑(Finset.Iic b) →
    Measurable f → DependsOn (ProbabilityTheory.Kernel.lmarginalPartialTraj κ a b f) ↑(Finset.Iic a)
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.limit_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type r}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)] [inst_5 : CategoryTheory.Limits.HasLimit F]
  (x y : CategoryTheory.ToType (CategoryTheory.Limits.limit F)),
  (∀ (j : J),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) y) →
    x = y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, k ∉ t₂ → (t₁ ∩ t₂).getKey! k = default
-- Lean.Compiler.IR.Basic
/-- We use `ctor` mainly for constructing Lean object/tobject values `lean_ctor_object` in the runtime.
This instruction is also used to creat `struct` and `union` return values.
For `union`, only `i.cidx` is relevant. For `struct`, `i` is irrelevant.  -/
Lean.IR.Expr.ctor : Lean.IR.CtorInfo → Array Lean.IR.Arg → Lean.IR.Expr
-- Mathlib.Topology.Connected.PathComponentOne
OpenNormalSubgroup.pathComponentOne.eq_1 : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : LocallyPathConnectedSpace G],
  OpenNormalSubgroup.pathComponentOne G = { toSubgroup := Subgroup.pathComponentOne G, isOpen' := ⋯, isNormal' := ⋯ }
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instZeroGroupSeminorm : {E : Type u_3} → [inst : Group E] → Zero (GroupSeminorm E)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
Differentiable.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {s : Set E}, Differentiable 𝕜 f → DifferentiableOn 𝕜 f s
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_aux.coe_fwdDiffₗ_pow : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (n : ℕ),
  ⇑(fwdDiff_aux.fwdDiffₗ M G h ^ n) = (fwdDiff h)^[n]
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- **Alias** of `MvPowerSeries.eq_zero_iff_forall_coeff_zero`. -/
MvPowerSeries.eq_zero_iff_forall_coeff_eq_zero_and : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R},
  f = 0 ↔ ∀ (d : σ →₀ ℕ), (MvPowerSeries.coeff d) f = 0
-- Init.Data.UInt.Lemmas
UInt16.neg_ne_zero : ∀ {a : UInt16}, -a ≠ 0 ↔ a ≠ 0
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedContext.default : Lean.Meta.Simp.Context
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.p_comm : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) f =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) g
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toHomeomorph_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
  [inst_7 : Module R₂ E₂], Function.Injective LinearIsometryEquiv.toHomeomorph
-- Init.System.IO
/-- File modification time.  -/
IO.FS.Metadata.modified : IO.FS.Metadata → IO.FS.SystemTime
-- Mathlib.Topology.Sets.Opens
/-- The preimage of an open set, as an open set.  -/
TopologicalSpace.Opens.comap : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → C(α, β) → FrameHom (TopologicalSpace.Opens β) (TopologicalSpace.Opens α)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterM.match_1.splitter : {β : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → n (ULift.{u_1, 0} Bool)} →
      [inst : MonadAttach n] →
        (out : β) →
          (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) →
            (__do_lift : Subtype (MonadAttach.CanReturn (f out))) →
              ((hf : MonadAttach.CanReturn (f out) { down := false }) → motive ⟨{ down := false }, hf⟩) →
                ((hf : MonadAttach.CanReturn (f out) { down := true }) → motive ⟨{ down := true }, hf⟩) →
                  motive __do_lift
-- Init.Data.String.Subslice
/-- The byte position of the start of the subslice.  -/
String.Slice.Subslice.startInclusive : {s : String.Slice} → s.Subslice → s.Pos
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.comapAddMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6}
  [inst_2 : AddZeroClass Z] (f : C(X, Y)) (g : LocallyConstant Y Z),
  (LocallyConstant.comapAddMonoidHom f) g = LocallyConstant.comap f g
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.instSmallCategoryElemObj : (Ω : Type w) → (S : CategoryTheory.SmallCategoryOfSet Ω) → CategoryTheory.SmallCategory ↑S.obj
-- Mathlib.Algebra.Ring.Defs
mul_two : ∀ {α : Type u} [inst : NonAssocSemiring α] (n : α), n * 2 = n + n
-- Mathlib.NumberTheory.MulChar.Duality
/-- **Alias** of `MulChar.domRestrictHom_surjective`.

---

Let `N` be a submonoid of `M` group and let `R` be a ring with enough roots of unity.
Then any `R`-value multiplicative character of `N` can be extended to a multiplicative
character of `M`.
 -/
MulChar.restrictHom_surjective : ∀ (M : Type u_1) (R : Type u_2) [inst : CommMonoid M] [inst_1 : CommRing R] [Finite M]
  [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] (N : Submonoid M), Function.Surjective ⇑(MulChar.domRestrictHom N R)
-- Lean.Meta.LitValues
/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt16` with value `n`.  -/
Lean.Meta.getUInt16Value? : Lean.Expr → Lean.MetaM (Option UInt16)
-- Mathlib.Analysis.MeanInequalities
NNReal.summable_mul_rpow_of_Lp_Lq : ∀ {ι : Type u} {f g : ι → NNReal} {p q r : ℝ},
  p.HolderTriple q r → (Summable fun i => f i ^ p) → (Summable fun i => g i ^ q) → Summable fun i => (f i * g i) ^ r
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.toSuggestion : Lean.TSyntax `tactic → Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.Analysis.Convex.Deriv
StrictMonoOn.exists_slope_lt_deriv : ∀ {x y : ℝ} {f : ℝ → ℝ},
  ContinuousOn f (Set.Icc x y) →
    x < y → StrictMonoOn (deriv f) (Set.Ioo x y) → ∃ a ∈ Set.Ioo x y, (f y - f x) / (y - x) < deriv f a
-- Mathlib.Data.Nat.Choose.Lucas
Choose.primeFactors_gcd_choose_of_isPrimePow : ∀ {n : ℕ}, IsPrimePow n → ((Finset.Icc 1 (n - 1)).gcd n.choose).primeFactors = {n.minFac}
-- Mathlib.RingTheory.Localization.Submodule
Algebra.EssFiniteType.isNoetherianRing : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S] [IsNoetherianRing R], IsNoetherianRing S
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.stabilizerEquivStabilizer.congr_simp : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g g_1 : G} (e_g : g = g_1) {a b : α}
  (hg : b = g • a), MulAction.stabilizerEquivStabilizer hg = MulAction.stabilizerEquivStabilizer ⋯
-- Plausible.Testable
Plausible.Testable.unusedVarTestable : {var : String} →
  {α : Sort u_1} →
    {β : Prop} → [Nonempty α] → [Plausible.Testable β] → Plausible.Testable (Plausible.NamedBinder var (∀ (a : α), β))
-- Mathlib.LinearAlgebra.Complex.Module
Complex.I_smul_mem_skewAdjoint_iff_isSelfAdjoint : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [StarModule ℂ A] {a : A},
  Complex.I • a ∈ skewAdjoint A ↔ IsSelfAdjoint a
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.map_mk_le : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M}
  {N : Type u_2} [inst_3 : AddCommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedAddMonoid N] (f : M →+o N),
  ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b → ArchimedeanClass.mk (f a) ≤ ArchimedeanClass.mk (f b)
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.exists_frobenius_solution_fractionRing_aux : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  (m n : ℕ) (r' q' : WittVector p k) (hr' : r'.coeff 0 ≠ 0) (hq' : q'.coeff 0 ≠ 0)
  (hq : ↑p ^ n * q' ∈ nonZeroDivisors (WittVector p k)),
  have b := WittVector.frobeniusRotation p hr' hq';
  (IsFractionRing.ringEquivOfRingEquiv (WittVector.frobeniusEquiv p k))
        ((algebraMap (WittVector p k) (FractionRing (WittVector p k))) b) *
      Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ =
    ↑p ^ (↑m - ↑n) * (algebraMap (WittVector p k) (FractionRing (WittVector p k))) b
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.opposite_inverse_obj : ∀ (α : Type u₁) (a : CategoryTheory.Discrete α), (CategoryTheory.Discrete.opposite α).inverse.obj a = Opposite.op a
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- The underlying lax prefunctor.  -/
CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.PrelaxFunctor B C → CategoryTheory.PrelaxFunctorStruct B C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_eq_zero_iff : ∀ {θ : Real.Angle}, θ.toReal = 0 ↔ θ = 0
-- Mathlib.Data.PNat.Basic
PNat.natPred_lt_natPred : ∀ {m n : ℕ+}, m.natPred < n.natPred ↔ m < n
-- Lean.EnvExtension
/-- Simple `PersistentEnvExtension` that implements `exportEntriesFn` using a list of entries.  -/
Lean.SimplePersistentEnvExtension : Type → Type → Type
-- Aesop.Util.UnorderedArraySet
_private.Aesop.Util.UnorderedArraySet.0.Aesop.UnorderedArraySet.mk.injEq : ∀ {α : Type u_1} [inst : BEq α] (rep rep_1 : Array α), ({ rep := rep } = { rep := rep_1 }) = (rep = rep_1)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- `p` is a Taylor series of `f` up to `n+1` if and only if `p.shift` is a Taylor series up to `n`
for `p 1`, which is a derivative of `f`. Version for `n : ℕ∞ω`.  -/
hasFTaylorSeriesUpToOn_succ_iff_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn (n + 1) f p s ↔
    (∀ x ∈ s, (p x 0).curry0 = f x) ∧
      (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
        HasFTaylorSeriesUpToOn n (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
/-- Another statement of the **Lefschetz principle**. A first-order sentence is modeled by the
theory of algebraically closed fields of characteristic zero if and only if it is modeled by the
theory of algebraically closed fields of characteristic `p` for all but finitely many primes `p`.
 -/
FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realize : ∀ {φ : FirstOrder.Language.ring.Sentence},
  FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ ↔ {p | FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}ᶜ.Finite
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.mapId_hom_app_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition]
  [inst_3 : P.IsMultiplicative] [inst_4 : Q.RespectsIso] (X : T)
  (f : optParam (X ⟶ X) (CategoryTheory.CategoryStruct.id X))
  (hf : autoParam (f = CategoryTheory.CategoryStruct.id X) CategoryTheory.MorphismProperty.Under.mapId._auto_1)
  (X_1 : P.Under Q X),
  ((CategoryTheory.MorphismProperty.Under.mapId Q X f hf).hom.app X_1).right =
    CategoryTheory.CategoryStruct.id X_1.right
-- Mathlib.NumberTheory.Modular
_private.Mathlib.NumberTheory.Modular.0.ModularGroup.case_c_one_d_one : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fd →
    g • z ∈ ModularGroup.fd →
      ‖UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g))
              ↑z‖ ≤
          1 →
        ↑g 1 0 = 1 →
          ↑g 1 1 = 1 →
            (g = ModularGroup.S * ModularGroup.T ∨ g = ModularGroup.T * ModularGroup.S * ModularGroup.T) ∧
              z = UpperHalfPlane.ρ
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_congr_nnnorm_ae : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  (∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊) → MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
-- Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
LinearMap.continuousAt_zero_of_locally_bounded : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [inst_3 : AddCommGroup F] [inst_4 : TopologicalSpace F] [inst_5 : NontriviallyNormedField 𝕜]
  [inst_6 : Module 𝕜 E] [ContinuousSMul 𝕜 E] [inst_8 : NormedField 𝕜'] [inst_9 : Module 𝕜' F] {σ : 𝕜 →+* 𝕜'}
  [RingHomIsometric σ] [FirstCountableTopology E] (f : E →ₛₗ[σ] F),
  (∀ (s : Set E), Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜' (⇑f '' s)) → ContinuousAt (⇑f) 0
-- Lean.Parser.Term
Lean.Parser.Term.ensureTypeOf.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Message
Lean.MessageData.instCoeMVarId : Coe Lean.MVarId Lean.MessageData
-- Mathlib.Combinatorics.Matroid.Basic
/-- There is at least one `Base`.  -/
Matroid.exists_isBase : ∀ {α : Type u_1} (self : Matroid α), ∃ B, self.IsBase B
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_hom_left_snd_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : T.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd R.hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.hom T.hom) S.hom))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.hom T.hom) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom) h
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of isomorphic additive magmas are isomorphic.  -/
AddSubsemigroup.centerCongr : {M : Type u_2} →
  {N : Type u_1} →
    [inst : Add M] → [inst_1 : Add N] → M ≃+ N → ↥(AddSubsemigroup.center M) ≃+ ↥(AddSubsemigroup.center N)
-- Mathlib.Order.Preorder.Chain
SuccChain.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (s : Set α),
  SuccChain r s = if h : ∃ t, IsChain r s ∧ SuperChain r s t then h.choose else s
-- Aesop.Tree.Data
Aesop.GoalData.mk.sizeOf_spec : ∀ {Rapp MVarCluster : Type} [inst : SizeOf Rapp] [inst_1 : SizeOf MVarCluster] (id : Aesop.GoalId)
  (parent : IO.Ref MVarCluster) (children : Array (IO.Ref Rapp)) (origin : Aesop.GoalOrigin) (depth : ℕ)
  (state : Aesop.GoalState) (isIrrelevant isForcedUnprovable : Bool) (preNormGoal : Lean.MVarId)
  (normalizationState : Aesop.NormalizationState) (mvars : Aesop.UnorderedArraySet Lean.MVarId)
  (forwardState : Aesop.ForwardState) (forwardRuleMatches : Aesop.ForwardRuleMatches)
  (successProbability : Aesop.Percent) (addedInIteration lastExpandedInIteration : Aesop.Iteration)
  (unsafeRulesSelected : Bool) (unsafeQueue : Aesop.UnsafeQueue) (failedRapps : Array Aesop.RegularRule),
  sizeOf
      { id := id, parent := parent, children := children, origin := origin, depth := depth, state := state,
        isIrrelevant := isIrrelevant, isForcedUnprovable := isForcedUnprovable, preNormGoal := preNormGoal,
        normalizationState := normalizationState, mvars := mvars, forwardState := forwardState,
        forwardRuleMatches := forwardRuleMatches, successProbability := successProbability,
        addedInIteration := addedInIteration, lastExpandedInIteration := lastExpandedInIteration,
        unsafeRulesSelected := unsafeRulesSelected, unsafeQueue := unsafeQueue, failedRapps := failedRapps } =
    1 + sizeOf id + sizeOf parent + sizeOf children + sizeOf origin + sizeOf depth + sizeOf state +
                              sizeOf isIrrelevant +
                            sizeOf isForcedUnprovable +
                          sizeOf preNormGoal +
                        sizeOf normalizationState +
                      sizeOf mvars +
                    sizeOf forwardState +
                  sizeOf forwardRuleMatches +
                sizeOf successProbability +
              sizeOf addedInIteration +
            sizeOf lastExpandedInIteration +
          sizeOf unsafeRulesSelected +
        sizeOf unsafeQueue +
      sizeOf failedRapps
-- Mathlib.Order.OrdContinuous
/-- Convert an injective right order continuous function to an order embedding.  -/
RightOrdContinuous.toOrderEmbedding : {α : Type u} →
  {β : Type v} →
    [inst : SemilatticeInf α] →
      [inst_1 : SemilatticeInf β] → (f : α → β) → RightOrdContinuous f → Function.Injective f → α ↪o β
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
/-- If `τ : G₁ ⟶ G₂` is a natural transformation between two bifunctors
which commute shifts on both variables, this typeclass asserts a compatibility of `τ`
with these shifts.  -/
CategoryTheory.NatTrans.CommShift₂ : {C₁ : Type u_1} →
  {C₂ : Type u_3} →
    {D : Type u_5} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D] →
            {M : Type u_6} →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : CategoryTheory.HasShift C₁ M] →
                  [inst_5 : CategoryTheory.HasShift C₂ M] →
                    [inst_6 : CategoryTheory.HasShift D M] →
                      {G₁ G₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} →
                        (G₁ ⟶ G₂) →
                          (h : CategoryTheory.CommShift₂Setup D M) → [G₁.CommShift₂ h] → [G₂.CommShift₂ h] → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_add_int_mul_pi : ∀ (x : ℂ) (n : ℤ), Complex.tan (x + ↑n * ↑Real.pi) = Complex.tan x
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- A normal cyclic Sylow subgroup is either central or contained in the commutator subgroup.  -/
Sylow.le_center_or_le_commutator : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite G] (P : Sylow p G) [IsCyclic ↥↑P] [(↑P).Normal],
  ↑P ≤ Subgroup.center G ∨ ↑P ≤ commutator G
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 64-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^64 - 1` for natural numbers greater than or equal to `2^64`.
 -/
UInt64.ofNatTruncate : ℕ → UInt64
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.Pos.skipWhile_char_eq_self_iff_get : ∀ {c : Char} {s : String.Slice} {pos : s.Pos}, pos.skipWhile c = pos ↔ ∀ (h : pos ≠ s.endPos), pos.get h ≠ c
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomAddAct.vadd_aeeqFun_const : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : VAdd M α] [inst_3 : MeasurableConstVAdd M α]
  [inst_4 : MeasureTheory.VAddInvariantMeasure M α μ] (c : Mᵈᵃᵃ) (b : β),
  c +ᵥ MeasureTheory.AEEqFun.const α b = MeasureTheory.AEEqFun.const α b
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.GenerateMeasurable.below.compl : ∀ {α : Type u_1} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.GenerateMeasurable s a → Prop} (t : Set α)
  (a : MeasurableSpace.GenerateMeasurable s t),
  MeasurableSpace.GenerateMeasurable.below a → motive t a → MeasurableSpace.GenerateMeasurable.below ⋯
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.mk.inj : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {inst : Semiring A} {inst_1 : Monoid G}
  {inst_2 : AddCommMonoid V} {inst_3 : AddCommMonoid W} {inst_4 : Module A V} {inst_5 : Module A W}
  {ρ : Representation A G V} {σ : Representation A G W} {toLinearMap : V →ₗ[A] W}
  {isIntertwining' : ∀ (g : G), toLinearMap ∘ₗ ρ g = σ g ∘ₗ toLinearMap} {toLinearMap_1 : V →ₗ[A] W}
  {isIntertwining'_1 : ∀ (g : G), toLinearMap_1 ∘ₗ ρ g = σ g ∘ₗ toLinearMap_1},
  { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' } =
      { toLinearMap := toLinearMap_1, isIntertwining' := isIntertwining'_1 } →
    toLinearMap = toLinearMap_1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.takeWhile_append_dropWhile : ∀ {ρ : Type} {pat : ρ} [String.Slice.Pattern.Model.PatternModel pat] [inst : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.LawfulForwardPattern pat] {s : String}, (s.takeWhile pat).copy ++ (s.dropWhile pat).copy = s
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- **Alias** of `BoundedContinuousFunction.domRestrict`.

---

Restrict the domain of a bounded continuous function to a set.  -/
BoundedContinuousFunction.restrict : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] → BoundedContinuousFunction α β → (s : Set α) → BoundedContinuousFunction (↑s) β
-- Init.Meta.Defs
/-- Syntax that represents an identifier.
 -/
Lean.Syntax.Ident : Type