mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Declaration
Lean.InductiveVal.isReflexiveEx : Lean.InductiveVal → Bool
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_ringEquiv_lpBCF : ∀ {α : Type u_1} {R : Type u_3} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : NonUnitalNormedRing R] (f : ↥(lp (fun x => R) ⊤)), ⇑(RingEquiv.lpBCF f) = ↑f
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.isClosed_preimage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ (s : Set Y), IsClosed s → IsClosed (f ⁻¹' s)
-- Mathlib.Data.Holor
/-- `CPRankMax N x` means `x` has CP rank at most `N`, that is,
it can be written as the sum of N holors of rank at most 1.  -/
Holor.CPRankMax : {α : Type} → [Mul α] → [AddMonoid α] → ℕ → {ds : List ℕ} → Holor α ds → Prop
-- Lean.Declaration
/-- List of all (including this one) declarations in the same mutual block.
 -/
Lean.ConstantInfo.all : Lean.ConstantInfo → List Lean.Name
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.InjectiveTheorem.mk.injEq : ∀ (levelParams : Array Lean.Name) (proof : Lean.Expr) (symbols : List Lean.HeadIndex) (origin : Lean.Meta.Grind.Origin)
  (levelParams_1 : Array Lean.Name) (proof_1 : Lean.Expr) (symbols_1 : List Lean.HeadIndex)
  (origin_1 : Lean.Meta.Grind.Origin),
  ({ levelParams := levelParams, proof := proof, symbols := symbols, origin := origin } =
      { levelParams := levelParams_1, proof := proof_1, symbols := symbols_1, origin := origin_1 }) =
    (levelParams = levelParams_1 ∧ proof = proof_1 ∧ symbols = symbols_1 ∧ origin = origin_1)
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Cardinal.mk_neg : ∀ {G : Type u_1} [inst : InvolutiveNeg G] (s : Set G), Cardinal.mk ↑(-s) = Cardinal.mk ↑s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.contains a = false → m.getKey? a = none
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMonObj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.MonObj M] {X Y₂ : Cᵒᵖ} (φ : X ⟶ Y₂),
  (CategoryTheory.yonedaMonObj M).map φ =
    MonCat.ofHom { toFun := fun x => CategoryTheory.CategoryStruct.comp φ.unop x, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Data.PNat.Factors
/-- Factoring a prime gives the corresponding one-element multiset.  -/
PNat.factorMultiset_ofPrime : ∀ (p : Nat.Primes), (↑p).factorMultiset = PrimeMultiset.ofPrime p
-- Mathlib.Algebra.Order.Module.Defs
le_inv_smul_iff_of_pos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β], 0 < a → (b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂)
-- Lean.Meta.Tactic.ElimInfo
/-- Gets all the eliminators defined using the `@[induction_eliminator]` and `@[cases_eliminator]` attributes.  -/
Lean.Meta.getCustomEliminators : Lean.CoreM Lean.Meta.CustomEliminators
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.Equiv.symm : ∀ {α : Type u} {s t : Stream'.WSeq α}, s ~ʷ t → t ~ʷ s
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.p_opcyclesMap'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) {Z : C}
  (h : h₂.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.p
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂) h) =
    CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.CategoryStruct.comp h₂.p h)
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.closure_range_union_range_eq_top : ∀ (R : Type uR) (A : Type uA) (B : Type uB) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B],
  Subring.closure (Set.range ⇑Algebra.TensorProduct.includeLeft ∪ Set.range ⇑Algebra.TensorProduct.includeRight) = ⊤
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The diagonal of a simplex is the long edge of the simplex.  -/
CategoryTheory.SimplicialObject.diagonal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.SimplicialObject C) →
      {n : ℕ} → X.obj (Opposite.op { len := n }) ⟶ X.obj (Opposite.op { len := 1 })
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Equivalence.isLeftAdjoint_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.functor.IsLeftAdjoint
-- Init.Conv
Lean.Parser.Tactic.Conv.argArg : Lean.ParserDescr
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instCoeSortType.eq_1 : GrpCat.instCoeSortType = { coe := GrpCat.carrier }
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.hasZeroMorphisms : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] →
              CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.DifferentialObject S C)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mem_inv : ∀ {α : Type u_2} [inst : Inv α] {s : Set α} {a : α}, a ∈ s⁻¹ ↔ a⁻¹ ∈ s
-- Mathlib.Data.List.Defs
/-- "Inhabited" `get` function: returns `default` instead of `none` in the case
that the index is out of bounds.  -/
List.getI : {α : Type u_1} → [Inhabited α] → List α → ℕ → α
-- Mathlib.Topology.Sheaves.Flasque
/-- Given a short exact sequence of sheaves, `0 ⟶ 𝓕 ⟶ 𝓖 ⟶ 𝓗 ⟶ 0`, if `𝓕` and `𝓖` are flasque,
then `𝓗` is flasque.  -/
TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂ : ∀ {X : TopCat} {S : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)},
  S.ShortExact → ∀ [S.X₁.IsFlasque] [S.X₂.IsFlasque], S.X₃.IsFlasque
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.type₁_dim : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j), (SSet.Subcomplex.Pairing.RankFunction.Cell.type₁ f c).dim = c.dim + 1
-- Mathlib.Topology.Algebra.Monoid
continuous_list_prod : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : Monoid M] [ContinuousMul M] {f : ι → X → M} (l : List ι),
  (∀ i ∈ l, Continuous (f i)) → Continuous fun a => (List.map (fun i => f i a) l).prod
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool} {k fallback : α},
  (Std.TreeSet.filter f t).getD k fallback = (Option.filter f (t.get? k)).getD fallback
-- Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots
instAlgebraAdjoinPthRoots : (k : Type u_1) → [inst : Field k] → Algebra k (AdjoinPthRoots k)
-- Mathlib.Analysis.Calculus.Implicit
/-- Any point in some neighborhood of `a` can be represented as `HasStrictFDerivAt.implicitFunction`
of some point.  -/
HasStrictFDerivAt.eq_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤),
  ∀ᶠ (x : E) in nhds a,
    HasStrictFDerivAt.implicitFunction f f' hf hf' (f x)
        (↑(HasStrictFDerivAt.implicitToOpenPartialHomeomorph f f' hf hf') x).2 =
      x
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_subset_interior_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.ball x ε ⊆ interior (Metric.closedBall x ε)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.instSemilinearIsometryClass : ∀ {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₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂], SemilinearIsometryClass (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
-- Mathlib.MeasureTheory.Measure.Lebesgue.Integral
/-- If two functions are integrable on a measurable set, and one function is less than
or equal to the other on that set, then the volume of the region
between the two functions can be represented as an integral.  -/
volume_regionBetween_eq_integral : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} {s : Set α}
  [MeasureTheory.SigmaFinite μ],
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ →
      MeasurableSet s →
        (∀ x ∈ s, f x ≤ g x) →
          (μ.prod MeasureTheory.volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- Given a predicate `P : Set J.obj → Prop` on the underlying type
of `J : CardinalDirectedPoset κ` such that all the subsets satisfying `P`
are `κ`-filtered, this is the cocone with point `J` given
by all the inclusions of the subsets satisfying `P`.  -/
CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    {J : CategoryTheory.CardinalDirectedPoset κ} →
      (P : Set ↑J.obj → Prop) →
        [inst_1 : ∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ] →
          CategoryTheory.Limits.Cocone (CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet P)
-- Mathlib.Algebra.Lie.TraceForm
LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieRing.IsNilpotent L] [IsDomain R] [Module.Free R M] [Module.Finite R M],
  (LieIdeal.toLieSubalgebra R L (LieModule.lowerCentralSeries R L L 1 ⊓ LieAlgebra.center R L)).toSubmodule ≤
    LinearMap.ker (LieModule.traceForm R L M)
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_sdiff : ∀ {V : Type u} {G : SimpleGraph V} (G₁ G₂ : G.Finsubgraph), ↑(G₁ \ G₂) = ↑G₁ \ ↑G₂
-- Mathlib.NumberTheory.RamificationInertia.Unramified
/-- A nonzero ideal of `R` is unramified in `S` if and only if every prime ideal of `S` lying
over it has ramification index `1`.  -/
Algebra.isUnramifiedIn_iff_forall_ramificationIdx_eq_one : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain R]
  [Module.Finite ℤ R] [CharZero R] [Algebra.EssFiniteType R S] [Algebra.IsIntegral R S] {𝔭 : Ideal R},
  Algebra.IsUnramifiedIn S 𝔭 ↔ ∀ (𝔓 : Ideal S) [𝔓.IsPrime], 𝔓.LiesOver 𝔭 → 𝔓.ramificationIdx R = 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- The quaternion conjugate maps to the "clifford conjugate" (aka `star`).  -/
CliffordAlgebraQuaternion.ofQuaternion_star : ∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R} (q : QuaternionAlgebra R c₁ 0 c₂),
  CliffordAlgebraQuaternion.ofQuaternion (star q) = star (CliffordAlgebraQuaternion.ofQuaternion q)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.restrict_iSup : ∀ {α : Type u_1} {ι : Sort u_3} (s : Set α) (m : ι → MeasureTheory.OuterMeasure α),
  (MeasureTheory.OuterMeasure.restrict s) (⨆ i, m i) = ⨆ i, (MeasureTheory.OuterMeasure.restrict s) (m i)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∈ m₂ → (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback
-- Init.Data.SInt.Lemmas
Int32.toInt8_ofNat' : ∀ {n : ℕ}, (Int32.ofNat n).toInt8 = Int8.ofNat n
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.basisOf_vadd : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (v : V) (b : AffineBasis ι k P), (v +ᵥ b).basisOf = b.basisOf
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_natCast : ∀ {R : Type u} [inst : Semiring R] {x : R} {n : ℕ}, Polynomial.eval x ↑n = ↑n
-- Init.PropLemmas
forall_const : ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], (∀ (a : α), b) ↔ b
-- Init.Data.Int.Linear
Int.Internal.Linear.div_eq : ∀ (a b k : ℤ), b = k → a / b = a / k
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- For the version where the first space in the product is countable,
see `measurable_from_prod_countable_right`.  -/
measurable_from_prod_countable_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  [Countable β] [MeasurableSingletonClass β] {f : α × β → γ}, (∀ (y : β), Measurable fun x => f (x, y)) → Measurable f
-- Init.Data.Nat.Basic
Nat.left_distrib : ∀ (n m k : ℕ), n * (m + k) = n * m + n * k
-- Mathlib.Geometry.Euclidean.Inversion.Basic
ContinuousAt.inversion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {X : Type u_3} [inst_4 : TopologicalSpace X] {c x : X → P} {R : X → ℝ} {a₀ : X},
  ContinuousAt c a₀ →
    ContinuousAt R a₀ →
      ContinuousAt x a₀ → x a₀ ≠ c a₀ → ContinuousAt (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) a₀
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.ExtDHashMap.Const.insertMany m l).getKey! k' = k
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
UpgradedStandardBorel.toPolishSpace : ∀ {α : Type u_1} [self : UpgradedStandardBorel α], PolishSpace α
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso_inv_app_app_f : ∀ (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] (X : CategoryTheory.Functor C D) (X_1 : C),
  (((CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso C D).inv.app X).app X_1).f =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.assocInv_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y}
  {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY)
  (s : CategoryTheory.Limits.BinaryFan X sYZ.pt),
  (CategoryTheory.Limits.BinaryFan.assocInv P s).fst =
    CategoryTheory.Limits.BinaryFan.IsLimit.lift P s.fst (CategoryTheory.CategoryStruct.comp s.snd sYZ.fst)
-- Mathlib.Data.List.MinMax
List.minimum_nil : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α], [].minimum = ⊤
-- Mathlib.Data.Sum.Order
Sum.Lex.inr_lt_inr_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : β}, toLex (Sum.inr a) < toLex (Sum.inr b) ↔ a < b
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.ProbabilityMeasure.toMeasure_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β), ↑(μ.prod ν) = (↑μ).prod ↑ν
-- Mathlib.Order.Defs.LinearOrder
/-- In a linearly ordered type, we assume the order relations are all decidable.  -/
LinearOrder.toDecidableLE : {α : Type u_2} → [self : LinearOrder α] → DecidableLE α
-- Mathlib.Algebra.Order.Chebyshev
/-- Special case of **Jensen's inequality** for sums of powers.  -/
pow_sum_div_card_le_sum_pow : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {f : ι → α},
  (∀ i ∈ s, 0 ≤ f i) → ∀ (n : ℕ), (∑ i ∈ s, f i) ^ (n + 1) / ↑s.card ^ n ≤ ∑ i ∈ s, f i ^ (n + 1)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_throw_lift_OptionT_apply_eq : ∀ {Pred : Type u} {EPred : Type u_1} {ε : Type u} {m : Type u → Type v} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : MonadExceptOf ε m] {α : Type u} {post : α → Pred}
  {epost : EPost.Cons✝ Pred EPred} (err : ε),
  Std.Internal.Do.wp (MonadExceptOf.throw err) post epost =
    Std.Internal.Do.wp (MonadExceptOf.throw err) (Std.Internal.Do.EPost.Cons.pushOption post epost) epost.tail
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.ReflGen.stdSymm`. -/
Relation.ReflGen.symmetric : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Std.Symm (Relation.ReflGen r)
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.coe_chainTop : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  ⇑(LieModule.chainTop α β) = ↑(LieModule.chainTopCoeff α β) • α + ⇑β
-- Mathlib.Order.Filter.Interval
Filter.Tendsto.uIcc : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {l : Filter α} [Filter.TendstoIxxClass Set.Icc l l] {f g : β → α}
  {lb : Filter β},
  Filter.Tendsto f lb l → Filter.Tendsto g lb l → Filter.Tendsto (fun x => Set.uIcc (f x) (g x)) lb l.smallSets
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_swap_sumElim : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α →₀ M) (g : β →₀ M),
  Finsupp.mapDomain Sum.swap (f.sumElim g) = g.sumElim f
-- Init.Data.Option.List
Option.length_toList_choice_eq_one : ∀ {α : Type u_1} [Nonempty α], (Option.choice α).toList.length = 1
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_cast_Iio : ∀ {n m : ℕ} (h : n = m) (i : Fin n), Finset.image (Fin.cast h) (Finset.Iio i) = Finset.Iio (Fin.cast h i)
-- Mathlib.MeasureTheory.Measure.Support
/-- A point `x` lies outside the support of `μ` iff some neighborhood of `x` has measure zero.  -/
MeasureTheory.Measure.notMem_support_iff_exists : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} {x : X},
  x ∉ μ.support ↔ ∃ U ∈ nhds x, μ U = 0
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.isQuotientMap_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsQuotientMap ⇑DomAddAct.mk.symm
-- Lean.Elab.Exception
Lean.Elab.abortTacticExceptionId : Lean.InternalExceptionId
-- Mathlib.Data.Nat.DvdSequence
Nat.IsStrongDvdSequence.const : ∀ (n : ℕ), Nat.IsStrongDvdSequence fun x => n
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
QuadraticMap.smul_toBilin : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : LinearOrder ι] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N] (S : Type u_5)
  [inst_6 : CommSemiring S] [inst_7 : Algebra S R] [inst_8 : Module S N] [inst_9 : IsScalarTower S R N]
  (bm : Module.Basis ι R M) (s : S) (Q : QuadraticMap R M N), (s • Q).toBilin bm = s • Q.toBilin bm
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedOrderHom α β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- An `InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D` bundles the
core data needed to construct a full `LawfulDayConvolutionMonoidalCategoryStructCore`.
We are making this a class so that it can act as a "proxy" for inferring `DayConvolution`
instances (which is all the more important that we are modifying the instances given in the
constructor to get better ones defeq-wise). As this object is purely about the internals
of definitions of Day convolutions monoidal structures, it is advised to not register
this class globally.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (V : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory V] →
            (D : Type u₃) → [CategoryTheory.Category.{v₃, u₃} D] → Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.connectivity_pos : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {S : Finset G},
  K < 1 → S.Nonempty → 0 < Finset.connectivity✝ K S
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Equivalence.isRightAdjoint_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.functor.IsRightAdjoint
-- Mathlib.CategoryTheory.Functor.Currying
/-- The equivalence of types of bifunctors giving by flipping the arguments.  -/
CategoryTheory.Functor.flippingEquiv : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} E] →
            CategoryTheory.Functor C (CategoryTheory.Functor D E) ≃
              CategoryTheory.Functor D (CategoryTheory.Functor C E)
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAtFilter.add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → HasDerivAtFilter g g' L → HasDerivAtFilter (f + g) (f' + g') L
-- Lean.Meta.Tactic.Ext
/-- Erases a name marked `ext` by adding it to the state's `erased` field and
removing it from the state's list of `Entry`s.

This is triggered by `attribute [-ext] name`.
 -/
Lean.Meta.Ext.ExtTheorems.eraseCore : Lean.Meta.Ext.ExtTheorems → Lean.Name → Lean.Meta.Ext.ExtTheorems
-- Init.Data.List.Basic
/-- If `l₁` is a subsequence of `l₂`, then it is also a subsequence of `a :: l₂`.  -/
List.Sublist.cons : ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → l₁.Sublist (a :: l₂)
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.stdSimplex.eq_boundary_iff : ∀ {n : ℕ} (A : (SSet.stdSimplex.obj { len := n }).Subcomplex), A = SSet.boundary n ↔ SSet.boundary n ≤ A ∧ A ≠ ⊤
-- Mathlib.Topology.Sheaves.Stalks
/-- A morphism from the stalk of `F` at `x` to some object `Y` is completely determined by its
composition with the `germ` morphisms.
 -/
TopCat.Presheaf.stalk_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {x : ↑X} {Y : C} {f₁ f₂ : F.stalk x ⟶ Y},
  (∀ (U : TopologicalSpace.Opens ↑X) (hxU : x ∈ U),
      CategoryTheory.CategoryStruct.comp (F.germ U x hxU) f₁ = CategoryTheory.CategoryStruct.comp (F.germ U x hxU) f₂) →
    f₁ = f₂
-- Lean.Meta.Tactic.Grind.EMatchTheoremParam
Lean.Meta.Grind.globalDeclToInstantiateParamSyntax : Lean.Name → Lean.Meta.Grind.EMatchTheoremKind → Bool → Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.Grind.thm)
-- Init.Data.List.Count
List.countP_tail_le : ∀ {α : Type u_1} {p : α → Bool} (l : List α), List.countP p l.tail ≤ List.countP p l