mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.sigPromise : Lean.Environment.AddConstAsyncResult → IO.Promise Lean.ConstantVal
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instIsOrderedSMulOfENNReal : ∀ {α : Type u_1} {R : Type u_6} {m0 : MeasurableSpace α} [inst : SMul R ENNReal] [inst_1 : LE R]
  [inst_2 : IsScalarTower R ENNReal ENNReal] [IsOrderedSMul R ENNReal], IsOrderedSMul R (MeasureTheory.Measure α)
-- Std.Http.Data.Body.Full
/-- Builds a request with an HTML body.
Sets `Content-Type: text/html; charset=utf-8`.
 -/
Std.Http.Request.Builder.html : Std.Http.Request.Builder → String → Std.Async.Async (Std.Http.Request Std.Http.Body.Full)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.algebraMapInv_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  SymmetricAlgebra.algebraMapInv ((SymmetricAlgebra.ι R M) x) = 0
-- Std.Http.Data.Body.Stream
/-- Reads all remaining chunks and decodes them into `α`.

Works in both `Async` (reads until EOF, no cancellation) and `ContextAsync` (also stops if the
context is cancelled).
 -/
Std.Http.Body.Stream.readAll : {α : Type} →
  {m : Type → Type} →
    [Std.Http.Body.FromByteArray α] →
      [Monad m] →
        [MonadExceptOf IO.Error m] →
          [Std.Http.Body.Stream.NextChunk m] → Std.Http.Body.Stream → optParam (Option UInt64) none → m α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_left_hom : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₂ : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom)
  (iso : f₁ ≅ f₁'), (sq₁₂.ι_iso_of_iso_left sq₁₂' iso).hom = sq₁₂.mapArrowLeft sq₁₂' iso.hom
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Convenience notation for the underlying arrow of a monomorphism over X.  -/
CategoryTheory.MonoOver.arrow : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → (f : CategoryTheory.MonoOver X) → f.obj.left ⟶ X
-- Mathlib.NumberTheory.Height.NumberField
/-- **Alias** of `NumberField.finite_setOfPred_mulHeight_nat_le`.

---

The set of `a : 𝓞 K` such that `mulHeight₁ (a / n) = mulHeight ![a, n]` is bounded
(for some given nonzero `n : ℕ`) is finite.  -/
NumberField.finite_setOf_mulHeight_nat_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {n : ℕ},
  n ≠ 0 → ∀ (B : ℝ), {a | Height.mulHeight ![↑a, ↑n] ≤ B}.Finite
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toProp.eq_5 : ∀ (K : Type u_2) [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K],
  FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.mulComm = ∀ (x y : K), x * y = y * x
-- Mathlib.Topology.Constructions
isClosedMap_toDual : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosedMap ⇑OrderDual.toDual
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prod_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α), (κ.prod η) a = (κ a).prod (η a)
-- Mathlib.Algebra.Field.Rat
NNRat.den_inv_of_ne_zero : ∀ {q : ℚ≥0}, q ≠ 0 → q⁻¹.den = q.num
-- Init.Prelude
/-- Converts a `Nat` into a `Char`. If the `Nat` does not encode a valid Unicode scalar value, `'\0'` is
returned instead.
 -/
Char.ofNat : ℕ → Char
-- Mathlib.RingTheory.Algebraic.Basic
/-- Transfer `Algebra.IsAlgebraic` across an `AlgEquiv`.  -/
AlgEquiv.isAlgebraic : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u_2}
  [inst_3 : Ring B] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B) [Algebra.IsAlgebraic R A], Algebra.IsAlgebraic R B
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Bicategory.leftUnitor η).hom.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
-- Init.NotationExtra
unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommSemiring.mk.injEq : ∀ (toSemiring : Lean.Meta.Grind.Arith.CommRing.Semiring) (ringId : ℕ) (commSemiringInst : Lean.Expr)
  (addRightCancelInst? : Option (Option Lean.Expr)) (toQFn? : Option Lean.Expr)
  (toSemiring_1 : Lean.Meta.Grind.Arith.CommRing.Semiring) (ringId_1 : ℕ) (commSemiringInst_1 : Lean.Expr)
  (addRightCancelInst?_1 : Option (Option Lean.Expr)) (toQFn?_1 : Option Lean.Expr),
  ({ toSemiring := toSemiring, ringId := ringId, commSemiringInst := commSemiringInst,
        addRightCancelInst? := addRightCancelInst?, toQFn? := toQFn? } =
      { toSemiring := toSemiring_1, ringId := ringId_1, commSemiringInst := commSemiringInst_1,
        addRightCancelInst? := addRightCancelInst?_1, toQFn? := toQFn?_1 }) =
    (toSemiring = toSemiring_1 ∧
      ringId = ringId_1 ∧
        commSemiringInst = commSemiringInst_1 ∧ addRightCancelInst? = addRightCancelInst?_1 ∧ toQFn? = toQFn?_1)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.map_genWeightSpace_le : ∀ {R : Type u_2} {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]
  [inst_7 : LieRing.IsNilpotent L] {M₂ : Type u_5} [inst_8 : AddCommGroup M₂] [inst_9 : Module R M₂]
  [inst_10 : LieRingModule L M₂] [inst_11 : LieModule R L M₂] {χ : L → R} (f : M →ₗ⁅R,L⁆ M₂),
  LieSubmodule.map f (LieModule.genWeightSpace M χ) ≤ LieModule.genWeightSpace M₂ χ
-- Mathlib.Order.Filter.Defs
Filter.mem_top_iff_forall : ∀ {α : Type u_1} {s : Set α}, s ∈ ⊤ ↔ ∀ (x : α), x ∈ s
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.MatcherKey.value : Lean.Meta.Match.MatcherKey✝ → Lean.Expr
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.mul_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {L : Type u_4} [inst_2 : NormedRing L] {f : α → L} {g : β → L},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g ν → MeasureTheory.Integrable (fun z => f z.1 * g z.2) (μ.prod ν)
-- Mathlib.Order.JordanHolder
RelSeries.eraseLast.eq_1 : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r),
  p.eraseLast = { length := p.length - 1, toFun := fun i => p.toFun ⟨↑i, ⋯⟩, step := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.toInt_ofInt_eq_self : ∀ {w : ℕ}, 0 < w → ∀ {n : ℤ}, -2 ^ (w - 1) ≤ n → n < 2 ^ (w - 1) → (BitVec.ofInt w n).toInt = n
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_pos : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {x : α},
  (CauSeq.const abs x).Pos ↔ 0 < x
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip' : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] {H : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} H]
  (F₁ : CategoryTheory.Functor B C) (F₂ : CategoryTheory.Functor D E) (G : CategoryTheory.Functor (C × E) H),
  CategoryTheory.Functor.uncurry.obj (F₁.comp (F₂.comp (CategoryTheory.Functor.curry.obj G).flip).flip) =
    (F₁.prod F₂).comp G
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.lit.injEq : ∀ (a a_1 : Lean.Literal), (Lean.Meta.LazyDiscrTree.Key.lit a = Lean.Meta.LazyDiscrTree.Key.lit a_1) = (a = a_1)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.piEquiv_apply : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] {ι' : Type u_7} {N : ι' → Type u_8} [inst_4 : (i : ι') → AddCommMonoid (N i)]
  [inst_5 : (i : ι') → TopologicalSpace (N i)] [inst_6 : (i : ι') → Module R (N i)] (f : (i : ι') → M [⋀^ι]→L[R] N i),
  ContinuousAlternatingMap.piEquiv f = ContinuousAlternatingMap.pi f
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.map_comp : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {T : Type u_3} {U : Type u_4} [inst_3 : Semiring T] [inst_4 : Semiring U]
  (w : AbsoluteValue T S) (u : AbsoluteValue U S) (f : R →+* T) (g : T →+* U),
  WithAbs.map v u (g.comp f) = (WithAbs.map w u g).comp (WithAbs.map v w f)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.many.sizeOf_spec : ∀ (name : Lean.Name) (type : Lean.Expr), sizeOf (Lean.Doc.ArgSpec.many✝ name type) = 1 + sizeOf name + sizeOf type
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.continuous_re : Continuous UpperHalfPlane.re
-- Std.Time.Time.Unit.Basic
/-- Converts a `Millisecond.Offset` to an `Hour.Offset`.
 -/
Std.Time.Hour.Offset.ofMilliseconds : Std.Time.Millisecond.Offset → Std.Time.Hour.Offset
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_natCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoMod hp a (b - ↑m * p) = toIcoMod hp a b
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.Q.liftOn₂.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] {β : Sort u_1} (q₁ q₂ : Lean.Grind.Ring.OfSemiring.Q α)
  (f : α × α → α × α → β)
  (h :
    ∀ {a₁ b₁ a₂ b₂ : α × α},
      Lean.Grind.Ring.OfSemiring.r α a₁ a₂ → Lean.Grind.Ring.OfSemiring.r α b₁ b₂ → f a₁ b₁ = f a₂ b₂),
  q₁.liftOn₂ q₂ f h = Quot.lift (fun a₁ => Quot.lift (f a₁) ⋯ q₂) ⋯ q₁
-- Mathlib.Algebra.Order.Kleene
kstar_mul_le_self : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a b : α}, a * b ≤ b → KStar.kstar a * b ≤ b
-- Aesop.Builder.Forward
Aesop.RuleBuilderOptions.forwardTransparency : Aesop.RuleBuilderOptions → Lean.Meta.TransparencyMode
-- Mathlib.Data.Num.Basic
/-- `bit1 x` appends a `1` to the end of `x`, mapping `x` to `2 * x + 1`.  -/
ZNum.bit1 : ZNum → ZNum
-- Lean.Meta.InferType
/-- `isPropQuickApp f n` is an "approximate" predicate which returns `LBool.true`
if `f` applied to `n` arguments is a proposition.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.isPropQuickApp : Lean.Expr → ℕ → Lean.MetaM Lean.LBool
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f' f) g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f' (CategoryTheory.Limits.pullback.fst f g))
      (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_W : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  (D₁ D₂ : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ), (D₁.sup D₂).W = D₁.W ⊔ D₂.W
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.comp : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {γ : Type u_8} {γ' : Type u_9} {_mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} {f : Ω → β} {g : Ω → β'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'}
  {_mγ : MeasurableSpace γ} {_mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'},
  ProbabilityTheory.IndepFun f g μ → Measurable φ → Measurable ψ → ProbabilityTheory.IndepFun (φ ∘ f) (ψ ∘ g) μ
-- Mathlib.RingTheory.Ideal.HasGoingUp
/-- [Stacks Tag 00HX](https://stacks.math.columbia.edu/tag/00HX) -/
Algebra.HasGoingUp.trans : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_5)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] [Algebra.HasGoingUp R S]
  [Algebra.HasGoingUp S T], Algebra.HasGoingUp R T
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.OfLocalizationSpanTarget.and : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.instLinearUliftFunctor : ∀ (R : Type u) [inst : CommRing R], CategoryTheory.Functor.Linear R (ModuleCat.uliftFunctor.{v', v, u} R)
-- Lean.Meta.Check
/-- Return true if `e` is type correct.
 -/
Lean.Meta.isTypeCorrect : Lean.Expr → Lean.MetaM Bool
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Dense.borel_eq_generateFrom_Ico_mem : ∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  [DenselyOrdered α] [NoMinOrder α] {s : Set α},
  Dense s → borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ico l u = S}
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.whiskerLeft_hom : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (C : CommAlgCat R) (f : A ⟶ B),
  CommAlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft C f) =
    Algebra.TensorProduct.map (AlgHom.id R ↑C) (CommAlgCat.Hom.hom f)
-- Mathlib.Analysis.Asymptotics.Completion
Asymptotics.isLittleO_completion_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F] {f : α → E}
  {g : α → F} {l : Filter α}, (fun x => ↑(g x)) =o[l] f ↔ g =o[l] f
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ : CategoryTheory.Functor J C}
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] (τ : F₁ ⟶ F₂) (j : J),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) τ)
      (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ j) =
    (CategoryTheory.eHomEquiv V) (τ.app j)
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
/-- A finset `s` such that `t = cylinder s S`. `S` is given by `closedCompactCylinders.set`.  -/
MeasureTheory.closedCompactCylinders.finset : {ι : Type u_1} →
  {X : ι → Type u_2} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {t : Set ((i : ι) → X i)} → t ∈ MeasureTheory.closedCompactCylinders X → Finset ι
-- Init.Data.Dyadic.Basic
/-- Convert a dyadic number to a rational number.  -/
Dyadic.toRat : Dyadic → ℚ
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- As an intermediate step to show that `μ.withDensity (v.limRatioMeas hρ) = ρ`, we show here
that `ρ ≤ t μ.withDensity (v.limRatioMeas hρ)` for any `t > 1`.  -/
VitaliFamily.le_mul_withDensity : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α]
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) {s : Set α},
  MeasurableSet s → ∀ {t : NNReal}, 1 < t → ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
-- Std.Internal.Do.WP.Basic
/-- Monotonicity: weaker postconditions yield weaker preconditions.  -/
Std.Internal.Do.WP.wp_trans_monotone : ∀ {Prog : Type u} {Value : outParam (Type v)} {Pred : outParam (Type w)} {EPred : outParam (Type w')}
  {inst : Std.Internal.Do.Assertion Pred} {inst_1 : Std.Internal.Do.Assertion EPred}
  [self : Std.Internal.Do.WP Prog Value Pred EPred] (x : Prog), (Std.Internal.Do.WP.wpTrans x).monotone
-- Mathlib.Geometry.Euclidean.Altitude
/-- The vector span of the opposite face lies in the direction
orthogonal to an altitude.  -/
Affine.Simplex.vectorSpan_isOrtho_altitude_direction : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  vectorSpan ℝ (s.points '' {i}ᶜ) ⟂ (s.altitude i).direction
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.mapIso_hom_π_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) {Z : C} (h : g b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (CategoryTheory.CategoryStruct.comp (p b).hom h)
-- Mathlib.RingTheory.LittleWedderburn
_private.Mathlib.RingTheory.LittleWedderburn.0.LittleWedderburn.InductionHyp.field : {D : Type u_1} →
  [inst : DivisionRing D] →
    LittleWedderburn.InductionHyp✝ D →
      {R : Subring D} → R < ⊤ → [Fintype D] → [DecidableEq D] → [DecidablePred fun x => x ∈ R] → Field ↥R
-- Mathlib.Topology.Instances.CantorSet
preCantorSet.eq_1 : preCantorSet 0 = Set.Icc 0 1
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.rightOpWhiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ D} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor D E} (α : F ⟶ G),
  CategoryTheory.NatTrans.rightOp (CategoryTheory.Functor.whiskerRight α H) =
    CategoryTheory.CategoryStruct.comp (G.rightOpComp H).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.rightOp α) H.op)
        (F.rightOpComp H).inv)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.rel : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (self : f.Homotopy g),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (SSet.stdSimplex.obj { len := 1 })) self.h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (SSet.stdSimplex.obj { len := 1 }))
      (CategoryTheory.CategoryStruct.comp φ B.ι)
-- Std.Time.Format.Modifier
Std.Time.Modifier.W.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.W presentation) = 1 + sizeOf presentation
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.ιInv.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorAlgebra.ιInv = TrivSqZeroExt.sndHom R M ∘ₗ TensorAlgebra.toTrivSqZeroExt.toLinearMap
-- Std.Time.Time.PlainTime
/-- Creates a new `PlainTime` by adjusting the `second` component to the given value.
 -/
Std.Time.PlainTime.withSeconds : Std.Time.PlainTime → Std.Time.Second.Ordinal true → Std.Time.PlainTime
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.struct : Lean.Lsp.CompletionItemKind
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.interpolatedStr.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.Quiver.Push
Quiver.PushQuiver.arrow.injEq : ∀ {V : Type u} [inst : Quiver V] {W : Type u₂} {σ : V → W} {X Y : V} (f f_1 : X ⟶ Y),
  (Quiver.PushQuiver.arrow f = Quiver.PushQuiver.arrow f_1) = (f = f_1)
-- Init.Tactics
/-- This is a "finishing" tactic modification of `simp`. It has two forms.

* `simpa [rules, ⋯] using e` will simplify the goal and the type of
  `e` using `rules`, then try to close the goal using `e`.

  Simplifying the type of `e` makes it more likely to match the goal
  (which has also been simplified). This construction also tends to be
  more robust under changes to the simp lemma set.

  The final match between the simplified `e` and the simplified goal uses
  **reducible** transparency, so it does not unfold semireducible definitions.
  Write `simpa [rules, ⋯] using! e` to perform the match at the ambient
  (default/semireducible) transparency instead.

* `simpa [rules, ⋯]` will simplify the goal and the type of a
  hypothesis `this` if present in the context, then try to close the goal using
  the `assumption` tactic.

As with `simp`, the `!` modifier after `simpa` enables auto-unfolding of
definitions in the simp set.
 -/
Lean.Parser.Tactic.simpaUsingBang : Lean.ParserDescr
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_sub_lt_of_leadingCoeff_eq : ∀ {A : Type u_3} {B : Type u_5} [inst : LinearOrder B] [inst_1 : OrderBot B] {D : A → B} [inst_2 : AddZeroClass A],
  Function.Injective D →
    ∀ {R : Type u_8} [inst_3 : Ring R] {p q : AddMonoidAlgebra R A},
      AddMonoidAlgebra.supDegree D p = AddMonoidAlgebra.supDegree D q →
        AddMonoidAlgebra.leadingCoeff D p = AddMonoidAlgebra.leadingCoeff D q →
          AddMonoidAlgebra.supDegree D (p - q) < AddMonoidAlgebra.supDegree D p ∨ p = q
-- Lean.Parser.Extension
Lean.Parser.isParserCategory : Lean.Environment → Lean.Name → Bool
-- Mathlib.Analysis.SpecialFunctions.Log.Base
_private.Mathlib.Analysis.SpecialFunctions.Log.Base.0.Real.b_ne_one : ∀ {b : ℝ}, b < 1 → b ≠ 1
-- Init.Data.String.Iterate
String.Slice.ByteIterator.instIteratorLoopUInt8OfMonad : {m : Type → Type u_1} →
  {n : Type u_2 → Type u_3} → [inst : Monad m] → [Monad n] → Std.IteratorLoop String.Slice.ByteIterator m n
-- Init.Data.Option.Basic
instFunctorOption : Functor Option
-- Mathlib.Order.Cover
wcovBy_iff_covBy_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b ↔ a ⋖ b ∨ a = b
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.QuasiIso.exact_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [CategoryTheory.ShortComplex.QuasiIso φ], S₁.Exact ↔ S₂.Exact
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = true → t.minKey! = default