mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.MapTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} [inst_2 : SizeOf α]
  (vec : aig.RefVec len) (func : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  [lawful : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref func]
  [chainable : Std.Sat.AIG.RefVec.LawfulMapOperator α func],
  sizeOf { vec := vec, func := func, lawful := lawful, chainable := chainable } =
    1 + sizeOf vec + sizeOf lawful + sizeOf chainable
-- Std.Internal.Do.ExceptPost
/-- An `EPost.Cons` value is below another if both components are below.  -/
Std.Internal.Do.EPost.Cons.mk_le : ∀ {e : Type u_1} {e' : Type u_2} [inst : Lean.Order.PartialOrder e] [inst_1 : Lean.Order.PartialOrder e'] (eposth : e)
  (epostt : e') (epost : EPost.Cons✝ e e'),
  Lean.Order.PartialOrder.rel eposth epost.head →
    Lean.Order.PartialOrder.rel epostt epost.tail → Lean.Order.PartialOrder.rel (EPost.Cons.mk✝ eposth epostt) epost
-- Lean.MetavarContext
Lean.MetavarContext.UnivMVarParamResult.mk.injEq : ∀ (mctx : Lean.MetavarContext) (newParamNames : Array Lean.Name) (nextParamIdx : ℕ) (expr : Lean.Expr)
  (mctx_1 : Lean.MetavarContext) (newParamNames_1 : Array Lean.Name) (nextParamIdx_1 : ℕ) (expr_1 : Lean.Expr),
  ({ mctx := mctx, newParamNames := newParamNames, nextParamIdx := nextParamIdx, expr := expr } =
      { mctx := mctx_1, newParamNames := newParamNames_1, nextParamIdx := nextParamIdx_1, expr := expr_1 }) =
    (mctx = mctx_1 ∧ newParamNames = newParamNames_1 ∧ nextParamIdx = nextParamIdx_1 ∧ expr = expr_1)
-- Init.Grind.AC
Lean.Grind.AC.Expr.op.injEq : ∀ (lhs rhs lhs_1 rhs_1 : Lean.Grind.AC.Expr), (lhs.op rhs = lhs_1.op rhs_1) = (lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Data.List.Cycle
List.prev_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (h : x ∈ [y]), [y].prev x h = y
-- Lean.Meta.CollectFVars
_private.Lean.Meta.CollectFVars.0.Lean.CollectFVars.State.addDependencies.getNext? : StateRefT' IO.RealWorld ℕ (StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM) (Option Lean.FVarId)
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.le_ord_iff : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {x : ↥X} (hx : Order.coheight x = 1) {f : ↑X.functionField},
  f ≠ 0 →
    ∀ {n : ℤ},
      n ≤ AlgebraicGeometry.Scheme.ord f x ↔ ↑(Multiplicative.ofAdd n) ≤ (AlgebraicGeometry.Scheme.ordHom x hx) f
-- Mathlib.Analysis.Normed.Group.Quotient
Ideal.Quotient.norm_mk_lt : ∀ {R : Type u_3} [inst : SeminormedCommRing R] {I : Ideal R} (x : R ⧸ I) {ε : ℝ},
  0 < ε → ∃ r, (Ideal.Quotient.mk I) r = x ∧ ‖r‖ < ‖x‖ + ε
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.setGcd.eq_1 : ∀ (s : Set ℕ), Nat.setGcd s = (Submodule.IsPrincipal.generator (Ideal.span (Nat.cast '' s))).natAbs
-- Mathlib.Algebra.Quaternion
instNontrivialQuaternion : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] [Nontrivial R], Nontrivial (Quaternion R)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorem.mk.sizeOf_spec : ∀ (keys : Array Lean.Meta.SimpTheoremKey) (levelParams : Array Lean.Name) (proof : Lean.Expr) (priority : ℕ)
  (post perm : Bool) (origin : Lean.Meta.Origin) (rfl backwardRfl : Bool),
  sizeOf
      { keys := keys, levelParams := levelParams, proof := proof, priority := priority, post := post, perm := perm,
        origin := origin, rfl := rfl, backwardRfl := backwardRfl } =
    1 + sizeOf keys + sizeOf levelParams + sizeOf proof + sizeOf priority + sizeOf post + sizeOf perm + sizeOf origin +
        sizeOf rfl +
      sizeOf backwardRfl
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Hover.mk.injEq : ∀ (contents : Lean.Lsp.MarkupContent) (range? : Option Lean.Lsp.Range) (contents_1 : Lean.Lsp.MarkupContent)
  (range?_1 : Option Lean.Lsp.Range),
  ({ contents := contents, range? := range? } = { contents := contents_1, range? := range?_1 }) =
    (contents = contents_1 ∧ range? = range?_1)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addLetToUnfold.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Lean.Elab.Tactic.ElabSimpArgResult.addLetToUnfold fvarId) = 1 + sizeOf fvarId
-- Std.Data.ExtDTreeMap.Lemmas
/-- Variant of `getD_map` that holds without `LawfulEqCmp`.  -/
Std.ExtDTreeMap.Const.getD_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} {fallback : γ},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.map f t) k fallback =
    (Option.pmap (fun v h => f (t.getKey k h) v) (Std.ExtDTreeMap.Const.get? t k) ⋯).getD fallback
-- Std.Data.ExtDTreeMap.Lemmas
_private.Std.Data.ExtDTreeMap.Lemmas.0.Std.ExtDTreeMap.Const.insertMany_list_mk : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {t : Std.DTreeMap α (fun x => β) cmp}
  {l : List (α × β)},
  Std.ExtDTreeMap.Const.insertMany (Std.ExtDTreeMap.mk t) l = Std.ExtDTreeMap.mk (Std.DTreeMap.Const.insertMany t l)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toListRev.go.aux₂ : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {it : Std.IterM m β} {acc : List β},
  Std.IterM.toListRev.go it acc = (fun x => x ++ acc) <$> it.toListRev
-- Mathlib.Data.Set.Card
/-- **Alias** of the reverse direction of `Set.encard_pos`. -/
Set.Nonempty.encard_pos : ∀ {α : Type u_1} {s : Set α}, s.Nonempty → 0 < s.encard
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.homologySequenceδ_quotient_mapTriangle_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj T) n₀ n₁ h =
    CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app T.obj₃)
      (CategoryTheory.CategoryStruct.comp
        ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯)
        ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app T.obj₁))
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.inv₀ : ∀ {α : Type u_1} {K : Type u_4} [inst : CommGroupWithZero K] [inst_1 : TopologicalSpace K] {f : α → K}
  {L : SummationFilter α} [ContinuousInv₀ K],
  Multipliable f L → ∏'[L] (x : α), f x ≠ 0 → Multipliable (fun x => (f x)⁻¹) L
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_sphere_comm : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, x ∈ Metric.sphere y ε ↔ y ∈ Metric.sphere x ε
-- Mathlib.Topology.UniformSpace.Ascoli
UniformOnFun.toFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)), UniformOnFun.toFun 𝔖 = (UniformOnFun.ofFun 𝔖).symm
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.zero_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  0 ∈ S
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.isCycleOn_one`. -/
Equiv.Perm.IsCycleOn.subsingleton : ∀ {α : Type u_2} {s : Set α}, Equiv.Perm.IsCycleOn 1 s → s.Subsingleton
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.memLp_top : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {m : MeasurableSpace E} [OpensMeasurableSpace E]
  {μ : MeasureTheory.Measure E} (f : TestFunction Ω F n), MeasureTheory.MemLp ⇑f ⊤ μ
-- Lean.Environment
/-- The main module data that will eventually be used to construct the kernel environment.  -/
_private.Lean.Environment.0.Lean.ImportedModule.mainModule? : Lean.ImportedModule✝ → Option Lean.ModuleData
-- Mathlib.Order.Disjoint
disjoint_of_le_iff_left_eq_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, a ≤ b → (Disjoint a b ↔ a = ⊥)
-- Mathlib.Combinatorics.Configuration
Configuration.Nondegenerate.mk : ∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L],
  (∀ (l : L), ∃ p, p ∉ l) →
    (∀ (p : P), ∃ l, p ∉ l) →
      (∀ {p₁ p₂ : P} {l₁ l₂ : L}, p₁ ∈ l₁ → p₂ ∈ l₁ → p₁ ∈ l₂ → p₂ ∈ l₂ → p₁ = p₂ ∨ l₁ = l₂) →
        Configuration.Nondegenerate P L
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Mon C} (f : X ⟶ Y) (x : CategoryTheory.Discrete PUnit.{w + 1}),
  ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).map f).hom.app x = f.hom
-- Mathlib.Order.Bounds.Basic
IsLUB.dual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α},
  IsLUB s a → IsGLB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
_private.Mathlib.AlgebraicTopology.SimplicialSet.HornColimits.0.SSet.horn.IsCompatible.multicofork.match_1.congr_eq_1 : ∀ {n : ℕ} {i : Fin (n + 2)} (motive : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ↑{i}ᶜ).R → Sort u_1)
  (x : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ↑{i}ᶜ).R)
  (h_1 : (j : Fin (n + 1 + 1)) → (hj : j ∈ {i}ᶜ) → motive ⟨j, hj⟩) (j : Fin (n + 1 + 1)) (hj : j ∈ {i}ᶜ),
  x = ⟨j, hj⟩ →
    (match x with
      | ⟨j, hj⟩ => h_1 j hj) ≍
      h_1 j hj
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.mk_snd_coe : ∀ {Δ Δ' : SimplexCategory} (f : Δ ⟶ Δ') [inst : CategoryTheory.Epi f],
  ↑(CategoryTheory.SimplicialObject.Splitting.IndexSet.mk f).snd = f
-- Mathlib.Data.Finset.Sigma
biSup_finsetSigma' : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset ι)
  (t : (i : ι) → Finset (α i)) (f : (i : ι) → α i → β), ⨆ i ∈ s, ⨆ j ∈ t i, f i j = ⨆ ij ∈ s.sigma t, f ij.fst ij.snd
-- Mathlib.Algebra.Order.Group.PosPart
/-- The *positive part* of an element `a` in a lattice ordered group is `a ⊔ 0`, denoted `a⁺`.  -/
instPosPart : {α : Type u_1} → [Lattice α] → [SubNegMonoid α] → PosPart α
-- Mathlib.Algebra.BigOperators.Finprod
finprod_subtype_eq_finprod_cond : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} (p : α → Prop),
  ∏ᶠ (j : Subtype p), f ↑j = ∏ᶠ (i : α) (_ : p i), f i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst : ∀ {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').inv
      (CategoryTheory.Limits.pullback.fst f' (CategoryTheory.Limits.pullback.fst f g)) =
    CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f' f) g
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.normedAddCommGroup.eq_1 : ∀ {E : Type u_2} [inst : NormedAddCommGroup E],
  OrderDual.normedAddCommGroup =
    { toNorm := OrderDual.toNorm, toAddCommGroup := OrderDual.instAddCommGroup,
      toMetricSpace := instMetricSpaceOrderDual, dist_eq := ⋯ }
-- Mathlib.Data.Vector.Basic
List.Vector.head_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (v : List.Vector α (n + 1)) (f : α → β), (List.Vector.map f v).head = f v.head
-- Mathlib.LinearAlgebra.Dimension.Finite
Module.finrank_eq_zero_of_not_faithfulSMul : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ¬FaithfulSMul R M → Module.finrank R M = 0
-- Mathlib.RepresentationTheory.Coinduced
Rep.instIsLeftAdjointResFunctor : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H),
  (Rep.resFunctor φ).IsLeftAdjoint
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNonUnitalSeminormedRing : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    [CompactSpace α] → {R : Type u_4} → [inst_2 : NonUnitalSeminormedRing R] → NonUnitalSeminormedRing C(α, R)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
OpenNormalSubgroup.toFiniteIndexNormalSubgroup_mono : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : CompactSpace G] [inst_3 : ContinuousMul G]
  {H K : OpenNormalSubgroup G}, H ≤ K → H.toFiniteIndexNormalSubgroup ≤ K.toFiniteIndexNormalSubgroup
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.hasSum : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
  (p : FormalMultilinearSeries 𝕜 E F) {x : E},
  x ∈ Metric.eball 0 p.radius → HasSum (fun n => (p n) fun x_1 => x) (p.sum x)
-- Init.Data.SInt.Lemmas
ISize.ofIntClamp_int8ToInt : ∀ (x : Int8), ISize.ofIntClamp x.toInt = x.toISize
-- Mathlib.Combinatorics.SetFamily.HarrisKleitman
/-- **Harris-Kleitman inequality**: Upper sets and lower sets of finsets anticorrelate.  -/
IsUpperSet.card_inter_le_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)} [inst_1 : Fintype α],
  IsUpperSet ↑𝒜 → IsLowerSet ↑ℬ → 2 ^ Fintype.card α * (𝒜 ∩ ℬ).card ≤ 𝒜.card * ℬ.card
-- Std.Time.Format
/-- Formats a `PlainDateTime` value into a `leanDateTime24Hour` format string.
 -/
Std.Time.PlainDateTime.toLeanDateTimeString : Std.Time.PlainDateTime → String
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R), (AddMonoidAlgebra.single m r).coeff = fun₀ | m => r
-- Lean.Parser.Command
Lean.Parser.Command.showDeprecatedModules.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Set.Lattice.Image
Set.bijOn_iInter_of_directed : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) s →
    ∀ {t : ι → Set β} {f : α → β}, (∀ (i : ι), Set.BijOn f (s i) (t i)) → Set.BijOn f (⋂ i, s i) (⋂ i, t i)
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Context.openDecls : Lean.PrettyPrinter.Delaborator.Context → List Lean.OpenDecl
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R),
  p.integralNormalization =
    p.sum fun i a => (Polynomial.monomial i) (if p.degree = ↑i then 1 else a * p.leadingCoeff ^ (p.natDegree - 1 - i))
-- Batteries.Tactic.Lint.Basic
/-- `errorsFound` is printed when at least one test is positive  -/
Batteries.Tactic.Lint.Linter.errorsFound : Batteries.Tactic.Lint.Linter → Lean.MessageData
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
/-- The additive equivalence between `H F 0` and the evaluation of `F` at a terminal object  -/
CategoryTheory.Sheaf.H.equiv₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
        [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] →
          (F : CategoryTheory.Sheaf J AddCommGrpCat) →
            {T : C} → CategoryTheory.Limits.IsTerminal T → F.H 0 ≃+ ↑(F.obj.obj (Opposite.op T))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {fallback : β k'} {f : β k → β k},
  m.WF →
    (m.modify k f).getD k' fallback =
      if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).getD fallback
      else m.getD k' fallback
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableVAdd₂.measurable_vadd : ∀ {M : Type u_2} {α : Type u_3} {inst : VAdd M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α}
  [self : MeasurableVAdd₂ M α], Measurable (Function.uncurry fun x1 x2 => x1 +ᵥ x2)
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.toFun_apply : ∀ {X Y : Type u} (f : TypeCat.Fun X Y) (x : X), f.toFun x = f x
-- Init.Data.Iterators.Basic
/-- A more convenient `cases` eliminator for `PlausibleIterStep`.
 -/
Std.PlausibleIterStep.casesOn : {α : Type u} →
  {β : Type w} →
    {IsPlausibleStep : Std.IterStep α β → Prop} →
      {motive : Std.PlausibleIterStep IsPlausibleStep → Sort x} →
        (s : Std.PlausibleIterStep IsPlausibleStep) →
          ((it' : α) →
              (out : β) → (h : IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
            ((it' : α) → (h : IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
              ((h : IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive s
-- Init.Data.Nat.Basic
Nat.sub_le_of_le_add : ∀ {a b c : ℕ}, a ≤ c + b → a - b ≤ c
-- Mathlib.Data.Num.Basic
/-- The type of nonnegative binary numbers, using `PosNum`.

```
13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))
```  -/
Num : Type
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.instDiscreteTopologyHomFintypeCatObj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C},
  DiscreteTopology (F.obj X ⟶ F.obj Y)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.DTreeMap.Raw.Const.ofList l cmp).isEmpty = l.isEmpty
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.ematch.sizeOf_spec : ∀ (origin : Lean.Meta.Grind.Origin), sizeOf (Lean.Meta.Grind.SplitSource.ematch origin) = 1 + sizeOf origin
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.category.sizeOf_spec : ∀ (catName declName : Lean.Name) (behavior : Lean.Parser.LeadingIdentBehavior),
  sizeOf (Lean.Parser.ParserExtension.OLeanEntry.category catName declName behavior) =
    1 + sizeOf catName + sizeOf declName + sizeOf behavior
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquivAlgOfEq_symm : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (h : I = J),
  (Ideal.quotientEquivAlgOfEq R₁ h).symm = Ideal.quotientEquivAlgOfEq R₁ ⋯
-- Mathlib.Order.Filter.Ker
Filter.ker_prod : ∀ {α : Type u_2} {β : Type u_3} (f : Filter α) (g : Filter β), (f ×ˢ g).ker = f.ker ×ˢ g.ker
-- Init.Data.Option.Attach
/-- “Attaches” a proof that some predicate holds for an optional value, if present, returning a subtype
that expresses this fact.

This function is primarily used to implement `Option.attach`, which allows definitions by
well-founded recursion that use iteration operators (such as `Option.map`) to prove that an optional
value drawn from a parameter is smaller than the parameter. This allows the well-founded recursion
mechanism to prove that the function terminates.
 -/
Option.attachWith : {α : Type u_1} → (xs : Option α) → (P : α → Prop) → (∀ (x : α), xs = some x → P x) → Option { x // P x }
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.succeeded.injEq : ∀ (goal : Lean.MVarId) (steps? : Option (Array Aesop.Script.LazyStep)) (goal_1 : Lean.MVarId)
  (steps?_1 : Option (Array Aesop.Script.LazyStep)),
  (Aesop.NormRuleResult.succeeded goal steps? = Aesop.NormRuleResult.succeeded goal_1 steps?_1) =
    (goal = goal_1 ∧ steps? = steps?_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.Type₁.isType₂_δ : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (s : SSet.prodStdSimplex.pairingCore.Type₁ k n),
  SSet.prodStdSimplex.pairingCore.IsType₂ s.δ
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.fromSum.eq_2 : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  (e₁ : c₁.Embedding c) (e₂ : c₂.Embedding c) (i₂ : ι₂),
  ComplexShape.Embedding.AreComplementary.fromSum e₁ e₂ (Sum.inr i₂) = e₂.f i₂
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.SatelliteConfig.centerAndRescale_radius : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {N : ℕ} {τ : ℝ}
  (a : Besicovitch.SatelliteConfig E N τ), a.centerAndRescale.r (Fin.last N) = 1
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.instL1SeminormedCommRing : {R : Type u_3} →
  {M : Type u_4} →
    [inst : SeminormedCommRing R] →
      [inst_1 : SeminormedAddCommGroup M] →
        [inst_2 : Module R M] →
          [inst_3 : Module Rᵐᵒᵖ M] →
            [IsCentralScalar R M] → [IsBoundedSMul R M] → SeminormedCommRing (TrivSqZeroExt R M)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.comp_zero_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.AddMonObj M] (f : X ⟶ Y) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp 0 h) = CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Topology.Inseparable
Specializes.map_of_continuousOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y}
  {s : Set X}, x ⤳ y → ContinuousOn f s → x ∈ s → y ∈ s → f x ⤳ f y
-- Batteries.Data.UInt
UInt16.le_iff_toNat_le_toNat : ∀ {x y : UInt16}, x ≤ y ↔ x.toNat ≤ y.toNat
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context.sym : Lean.Elab.Tactic.Grind.Context → Bool
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
IsCovariantDerivativeOn.iUnion : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] {ι : Type u_7}
  {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s : ι → Set M},
  (∀ (i : ι), IsCovariantDerivativeOn F cov (s i)) → IsCovariantDerivativeOn F cov (⋃ i, s i)
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Definition of the positive part of the logarithm, formulated as a theorem.  -/
Real.posLog_apply : ∀ {x : ℝ}, x.posLog = max 0 (Real.log x)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G),
  CochainComplex.HomComplex.Cochain.ofHom φ = CochainComplex.HomComplex.Cochain.ofHoms fun p => φ.f p
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀Inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (W : CategoryTheory.MorphismProperty C) {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
  [inst_6 : L.CommShift M] {X Y : C} [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y X]
  [inst_8 : W.RespectsIso] (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) (hf : W f),
  (CategoryTheory.Localization.SmallShiftedHom.equiv W L)
      (CategoryTheory.Localization.SmallShiftedHom.mk₀Inv m₀ hm₀ f hf) =
    CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (CategoryTheory.Localization.isoOfHom L W f hf).inv