mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `Multiseries`-part of `MultiseriesExpansion.one`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl
-- Mathlib.NumberTheory.Bertrand
/-- The inequality which contradicts Bertrand's postulate, for large enough `n`.
 -/
bertrand_main_inequality : ∀ {n : ℕ}, 512 ≤ n → n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
-- Init.Prelude
Nat.lt_of_le_of_lt : ∀ {n m k : ℕ}, n ≤ m → m < k → n < k
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive`.

---

Strongly progressive process. A sequence of functions `u` is said to be strongly
progressive with respect to a filtration `f` if at each point in time `i`, `u` restricted to
`Set.Iic i × Ω` is strongly measurable with respect to the product `MeasurableSpace` structure
where the σ-algebra used for `Ω` is `f i`.
The usual definition uses the interval `[0,i]`, which we replace by `Set.Iic i`. We recover the
usual definition for index types `ℝ≥0` or `ℕ`.  -/
MeasureTheory.ProgMeasurable : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        {β : Type u_3} → [TopologicalSpace β] → [MeasurableSpace ι] → MeasureTheory.Filtration ι m → (ι → Ω → β) → Prop
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux2.match_1.splitter : (motive : ONote × ℕ → Sort u_1) →
  (x : ONote × ℕ) → ((b : ONote) → motive (b, 0)) → ((b : ONote) → (k : ℕ) → motive (b, k.succ)) → motive x
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.IsSymmetric.C : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (r : R), (MvPolynomial.C r).IsSymmetric
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.ofHom_injective : ∀ {X Y : Type u} [inst : CommGroup X] [inst_1 : CommGroup Y], Function.Injective fun f => CommGrpCat.ofHom f
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.isEquivalence_right_of_isEquivalence_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.IsEquivalence], R.IsEquivalence
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Given a mono factorisation `X ⟶ I ⟶ Y` of an arrow `f`, an isomorphism `I ≅ I'` gives a new mono
factorisation `X ⟶ I' ⟶ Y` of `f`.
 -/
CategoryTheory.Limits.MonoFactorisation.ofIsoI : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (F : CategoryTheory.Limits.MonoFactorisation f) →
          {I' : C} → (F.I ≅ I') → CategoryTheory.Limits.MonoFactorisation f
-- Mathlib.Topology.Piecewise
continuous_if' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {p : α → Prop}
  [inst_2 : (a : α) → Decidable (p a)],
  (∀ a ∈ frontier {x | p x}, Filter.Tendsto f (nhdsWithin a {x | p x}) (nhds (if p a then f a else g a))) →
    (∀ a ∈ frontier {x | p x}, Filter.Tendsto g (nhdsWithin a {x | ¬p x}) (nhds (if p a then f a else g a))) →
      ContinuousOn f {x | p x} → ContinuousOn g {x | ¬p x} → Continuous fun a => if p a then f a else g a
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.neg_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R}, x ∈ I → -x ∈ I
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The star subalgebra of `C(UnitAddTorus d, ℂ)` generated by `mFourier n` for `n ∈ ℤᵈ`.  -/
UnitAddTorus.mFourierSubalgebra : (d : Type u_2) → [Fintype d] → StarSubalgebra ℂ C(UnitAddTorus d, ℂ)
-- Mathlib.Probability.Kernel.CondDistrib
/-- **Regular conditional probability distribution**: kernel associated with the conditional
expectation of `Y` given `X`.
For almost all `a`, `condDistrib Y X μ` evaluated at `X a` and a measurable set `s` is equal to
the conditional expectation `μ⟦Y ⁻¹' s | mβ.comap X⟧ a`. It also satisfies the equality
`μ[(fun a => f (X a, Y a)) | mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂(condDistrib Y X μ (X a))`
for all integrable functions `f`.  -/
ProbabilityTheory.condDistrib : {α : Type u_5} →
  {β : Type u_6} →
    {Ω : Type u_7} →
      [inst : MeasurableSpace Ω] →
        [StandardBorelSpace Ω] →
          [Nonempty Ω] →
            {x : MeasurableSpace α} →
              [inst_3 : MeasurableSpace β] →
                (α → Ω) →
                  (α → β) →
                    (μ : MeasureTheory.Measure α) → [MeasureTheory.IsFiniteMeasure μ] → ProbabilityTheory.Kernel β Ω
-- Mathlib.Analysis.Real.Spectrum
SpectrumRestricts.nnreal_of_nonneg : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] [inst_2 : PartialOrder A] [NonnegSpectrumClass ℝ A] {a : A},
  0 ≤ a → SpectrumRestricts a ⇑ContinuousMap.realToNNReal
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.concat_NonnegCoeffs : ∀ {p₁ p₂ : Lean.Grind.CommRing.Poly}, p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.concat p₂).NonnegCoeffs
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.sub_iff_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₂ =o[l] g → ((fun x => f₁ x - f₂ x) =o[l] g ↔ f₁ =o[l] g)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Basic
/-- Use the coherence theorem for monoidal categories to solve equations in a monoidal category,
where the two sides only differ by replacing strings of monoidal structural morphisms
(that is, associators, unitors, and identities)
with different strings of structural morphisms with the same source and target.

That is, `monoidal` can handle goals of the form
`a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'`
where `a = a'`, `b = b'`, and `c = c'` can be proved using `monoidal_coherence`.
 -/
Mathlib.Tactic.Monoidal.monoidal : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Std.Http.Protocol.H1.Event
/-- Signals that additional input data is required to continue processing.
 -/
Std.Http.Protocol.H1.Event.needMoreData : {dir : Std.Http.Protocol.H1.Direction} → Option ℕ → Std.Http.Protocol.H1.Event dir
-- Init.Data.Rat.Lemmas
/-- `Rat.ofScientific` applied to numeric literals is the same as a scientific literal.  -/
Rat.ofScientific_ofNat_ofNat : ∀ {m : ℕ} {s : Bool} {e : ℕ}, Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e
-- Lean.Meta.Tactic.Split
Lean.Meta.Split.throwDiscrGenError : {α : Type} → Lean.Expr → Lean.MetaM α
-- Init.Data.SInt.Bitwise
Int64.toInt8_and : ∀ (a b : Int64), (a &&& b).toInt8 = a.toInt8 &&& b.toInt8
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_eq_getElem?_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.minKey? = t.keysArray[0]?
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.twoPowShift : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget aig w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Order.Cofinal
not_isCofinal_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, ¬IsCofinal s ↔ ∃ x, ∀ y ∈ s, y < x
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_of_eq : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (p₁ : Int.Internal.Linear.Poly) (d₂ : ℤ)
  (p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.dvd_of_eq_cert x p₁ d₂ p₂ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ = 0 → d₂ ∣ Int.Internal.Linear.Poly.denote' ctx p₂
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.congr_simp : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m m_1 : ℕ} (e_m : m = m_1) (f_deg : f ∈ 𝒜 m)
  (q q_1 :
    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
            (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace),
  q = q_1 →
    ∀ (a a_1 : A),
      a = a_1 →
        AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q a =
          AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier ⋯ q_1 a_1
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.hom_inv_apply : ∀ {X Y : FinBddDistLat} (e : X ≅ Y) (s : ↑Y.toDistLat),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Algebra.Lie.Basis.Basic
/-- A basis has a natural involution obtained by interchanging the roles of `e` and `f` and
negating `h`.  -/
LieAlgebra.Basis.symm : {ι : Type u_1} →
  {R : Type u_2} →
    {L : Type u_3} →
      [inst : Finite ι] →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] →
            [inst_3 : LieAlgebra R L] → {H : LieSubalgebra R L} → LieAlgebra.Basis ι H → LieAlgebra.Basis ι H
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Path.brecOn.go : {α : Type u} →
  {motive : RBTree.RBNode.Path α → Sort u_1} →
    (t : RBTree.RBNode.Path α) →
      ((t : RBTree.RBNode.Path α) → RBTree.RBNode.Path.below t → motive t) → motive t ×' RBTree.RBNode.Path.below t
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- A non-computable version of `MonoidHom.liftOfRightInverse` for when no computable right
inverse is available, that uses `Function.surjInv`.  -/
MonoidHom.liftOfSurjective : {G₁ : Type u_5} →
  {G₂ : Type u_6} →
    {G₃ : Type u_7} →
      [inst : Group G₁] →
        [inst_1 : Group G₂] →
          [inst_2 : Group G₃] → (f : G₁ →* G₂) → Function.Surjective ⇑f → { g // f.ker ≤ g.ker } ≃ (G₂ →* G₃)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_iSup₂ : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {κ : Sort u_4}
  {κ' : κ → Sort u_5} (s : (i : κ) → κ' i → HomogeneousIdeal 𝒜), (⨆ i, ⨆ j, s i j).toIdeal = ⨆ i, ⨆ j, (s i j).toIdeal
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.continuousOn_smul : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] {𝕜 : Type u_9}
  [inst_6 : NormedRing 𝕜] [SecondCountableTopologyEither X 𝕜] [inst_8 : Module 𝕜 E] [IsBoundedSMul 𝕜 E] {f : X → E}
  {g : X → 𝕜} {s : Set X},
  IsLocallyClosed s →
    MeasureTheory.LocallyIntegrableOn f s μ →
      ContinuousOn g s → MeasureTheory.LocallyIntegrableOn (fun x => g x • f x) s μ
-- Mathlib.Algebra.Module.Submodule.LinearMap
Submodule.coe_inclusion : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M} (h : p ≤ p') (x : ↥p), ↑((Submodule.inclusion h) x) = ↑x
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.centralizer_le : ∀ {G : Type u_1} [inst : Group G] {s t : Set G}, s ⊆ t → Subgroup.centralizer t ≤ Subgroup.centralizer s
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ext_iff : ∀ (p : ENNReal) {V : Type u_4} {x y : WithLp p V}, x = y ↔ x.ofLp = y.ofLp
-- Lean.Elab.PreDefinition.WF.Preprocess
Lean.wf.preprocess : Lean.Option Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_subset_vadd_right : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s₁ s₂ : Set α} {t : Set β}, s₁ ⊆ s₂ → s₁ +ᵥ t ⊆ s₂ +ᵥ t
-- Init.Data.Vector.Lemmas
Vector.getElem_of_getElem? : ∀ {α : Type u_1} {n i : ℕ} {a : α} {xs : Vector α n}, xs[i]? = some a → ∃ (h : i < n), xs[i] = a
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial_two_mul : ∀ (n : ℕ), (2 * n).doubleFactorial = 2 ^ n * n.factorial
-- Init.Data.BitVec.Bitblast
BitVec.bit_not_add_self : ∀ {w : ℕ} (x : BitVec w), (BitVec.iunfoldr (fun i c => (c, !x[↑i])) ()).2 + x = -1
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mem_coeIdeal : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {x : P} {I : Ideal R}, x ∈ ↑I ↔ ∃ x' ∈ I, (algebraMap R P) x' = x
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.toSubgroup_injective : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G], Function.Injective ClosedSubgroup.toSubgroup
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Any morphism `k : Y ⟶ W` satisfying `f ≫ k = g ≫ k` factors through the coequalizer of `f`
and `g` via `coequalizer.desc : coequalizer f g ⟶ W`.  -/
CategoryTheory.Limits.coequalizer.desc : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] →
          {W : C} →
            (k : Y ⟶ W) →
              CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k →
                (CategoryTheory.Limits.coequalizer f g ⟶ W)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Filter.Tendsto.ennrpow_const : ∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} (r : ℝ),
  Filter.Tendsto m f (nhds a) → Filter.Tendsto (fun x => m x ^ r) f (nhds (a ^ r))
-- Init.Data.Slice.Lemmas
_private.Init.Data.Slice.Lemmas.0.Std.Slice.toList.eq_1 : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  (s : Std.Slice γ), s.toList = (Std.Slice.Internal.iter s).toList
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_neg : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.Chebyshev.U R (-n) = -Polynomial.Chebyshev.U R (n - 2)
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.ext_iff : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] {e₁ e₂ : M ≃ₗ⁅R,L⁆ N}, e₁ = e₂ ↔ ∀ (m : M), e₁ m = e₂ m
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
instIsFractionRingQuotientIdealResidueField : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime], IsFractionRing (R ⧸ I) I.ResidueField
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftAux_id_apply : ∀ {K : Type u_1} {M : Type u_3} [inst : CommSemiring K] [inst_1 : CommSemiring M] (j : K →+* M) (p : ℕ)
  [inst_2 : ExpChar M p] [inst_3 : PerfectRing M p] (x : K), PerfectRing.liftAux (RingHom.id K) j p x = j x
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.Premise.fvar.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId),
  (Mathlib.Tactic.ClickSuggestions.Premise.fvar fvarId = Mathlib.Tactic.ClickSuggestions.Premise.fvar fvarId_1) =
    (fvarId = fvarId_1)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      (it : Std.IterM m β) →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.CategoryTheory.Monoidal.Limits.Colimits
/-- The external tensor product of two cocones.  -/
CategoryTheory.Limits.Cocone.tensor₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {J₁ : Type u_3} →
        {J₂ : Type u_4} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} J₁] →
            [inst_3 : CategoryTheory.Category.{v_4, u_4} J₂] →
              {F₁ : CategoryTheory.Functor J₁ C} →
                {F₂ : CategoryTheory.Functor J₂ C} →
                  CategoryTheory.Limits.Cocone F₁ →
                    CategoryTheory.Limits.Cocone F₂ →
                      CategoryTheory.Limits.Cocone (CategoryTheory.MonoidalCategory.externalProduct F₁ F₂)
-- Init.MetaTypes
Lean.Meta.instBEqEtaStructMode : BEq Lean.Meta.EtaStructMode
-- Mathlib.Combinatorics.Young.YoungDiagram
_private.Mathlib.Combinatorics.Young.YoungDiagram.0.YoungDiagram.cellsOfRowLens.match_1.eq_1 : ∀ (motive : List ℕ → Sort u_1) (h_1 : Unit → motive []) (h_2 : (w : ℕ) → (ws : List ℕ) → motive (w :: ws)),
  (match [] with
    | [] => h_1 ()
    | w :: ws => h_2 w ws) =
    h_1 ()
-- Lean.Attributes
Lean.ParametricAttributeImpl.mk.injEq : ∀ {α : Type} (toAttributeImplCore : Lean.AttributeImplCore) (getParam : Lean.Name → Lean.Syntax → Lean.AttrM α)
  (afterSet : Lean.Name → α → Lean.AttrM Unit) (preserveOrder : Bool)
  (filterExport : Lean.Environment → Lean.Name → α → Bool) (toAttributeImplCore_1 : Lean.AttributeImplCore)
  (getParam_1 : Lean.Name → Lean.Syntax → Lean.AttrM α) (afterSet_1 : Lean.Name → α → Lean.AttrM Unit)
  (preserveOrder_1 : Bool) (filterExport_1 : Lean.Environment → Lean.Name → α → Bool),
  ({ toAttributeImplCore := toAttributeImplCore, getParam := getParam, afterSet := afterSet,
        preserveOrder := preserveOrder, filterExport := filterExport } =
      { toAttributeImplCore := toAttributeImplCore_1, getParam := getParam_1, afterSet := afterSet_1,
        preserveOrder := preserveOrder_1, filterExport := filterExport_1 }) =
    (toAttributeImplCore = toAttributeImplCore_1 ∧
      getParam = getParam_1 ∧ afterSet = afterSet_1 ∧ preserveOrder = preserveOrder_1 ∧ filterExport = filterExport_1)
-- Mathlib.Order.Monotone.Monovary
monovaryOn_iff_monovary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f g s ↔ Monovary (fun i => f ↑i) fun i => g ↑i
-- Aesop.RuleTac.Basic
/-- The result of a rule tactic is a list of rule applications.
 -/
Aesop.RuleTacOutput : Type
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_coe : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G'.coe.edgeSet = Sym2.map Subtype.val ⁻¹' G'.edgeSet
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.not_insertIfNew_eq_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, ¬m.insertIfNew k v = ∅
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_bot_right : ∀ {G : Type u_1} [inst : Group G] (H₁ : Subgroup G), ⁅H₁, ⊥⁆ = ⊥
-- Mathlib.Algebra.Regular.ULift
ULift.isRightRegular_down : ∀ {R : Type v} [inst : Mul R] {a : ULift.{u, v} R}, IsRightRegular a.down ↔ IsRightRegular a
-- Mathlib.Data.Fin.Parity
Fin.not_odd_iff_even_of_even : ∀ {n : ℕ} {k : Fin n} [inst : NeZero n], Even n → (¬Odd k ↔ Even k)
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.smul_subset_self : ∀ {α : Type u_1} (s : Multiset α) (n : ℕ), n • s ⊆ s
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- Chain rule for polynomials viewed as power series.  Use `derivative_subst` instead.  -/
_private.Mathlib.RingTheory.PowerSeries.Derivative.0.PowerSeries.derivative_subst_coe : ∀ {R : Type u_1} [inst : CommRing R] (p : Polynomial R) {g : PowerSeries R},
  PowerSeries.HasSubst g →
    (PowerSeries.derivative R) (PowerSeries.subst g ↑p) =
      PowerSeries.subst g ((PowerSeries.derivative R) ↑p) * (PowerSeries.derivative R) g
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedDep.mk.inj : ∀ {name : Lean.Name} {ident : Lean.TSyntax `ident} {binderType : Lean.TSyntax `term} {isClass : Bool}
  {name_1 : Lean.Name} {ident_1 : Lean.TSyntax `ident} {binderType_1 : Lean.TSyntax `term} {isClass_1 : Bool},
  { name := name, ident := ident, binderType := binderType, isClass := isClass } =
      { name := name_1, ident := ident_1, binderType := binderType_1, isClass := isClass_1 } →
    name = name_1 ∧ ident = ident_1 ∧ binderType = binderType_1 ∧ isClass = isClass_1
-- Mathlib.RingTheory.IsAdjoinRoot
AdjoinRoot.isAdjoinRoot_root_eq_root : ∀ {R : Type u} [inst : CommRing R] (f : Polynomial R), (AdjoinRoot.isAdjoinRoot f).root = AdjoinRoot.root f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany_eq_foldl : ∀ {α : Type u} {β : Type v} {x : Ord α} {l : List (α × β)} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  (h : t.Balanced),
  ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l h) =
    List.foldl
      (fun acc x_1 =>
        match x_1 with
        | (k, v) => Std.DTreeMap.Internal.Impl.insert! k v acc)
      t l
-- Mathlib.RingTheory.Ideal.Maps
LinearMap.annihilator_le_of_injective : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Function.Injective ⇑f → Module.annihilator R M' ≤ Module.annihilator R M
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_iInf_le : ∀ {G : Type u_1} [inst : Group G] {L : Subgroup G} {ι : Type u_3} [inst_1 : Fintype ι] (f : ι → Subgroup G),
  (⨅ i, f i).relIndex L ≤ ∏ i, (f i).relIndex L
-- Lean.Meta.Tactic.Assert
/-- Like `Lean.MVarId.assertAfter`, but asserts the new hypothesis at the earliest point after `fvarId`
where `type` is well-formed. Note that `val` may depend on any variables in the local context.

The expression `type` may contain metavariables, and this procedure ensures they are well-formed
at the point in the local context where the hypothesis is asserted.
The metavariables in `type` are instantiated to avoid false dependencies.
 -/
Lean.MVarId.assertAfter' : Lean.MVarId → Lean.FVarId → Lean.Name → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Meta.AssertAfterResult
-- Mathlib.Algebra.Group.End
Equiv.Perm.extendDomainHom_apply : ∀ {α : Type u_4} {β : Type u_5} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (e : Equiv.Perm α),
  (Equiv.Perm.extendDomainHom f) e = e.extendDomain f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_2 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (distance : ℕ) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.rotateLeft distance with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_2 distance