mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.map_span : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : Set M),
  Submodule.map f (Submodule.span R s) = Submodule.span R₂ (⇑f '' s)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.isoMk_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (h : V₀.V ≅ V₁.V)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp V₀.str (F.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom V₁.str)
      CategoryTheory.Endofunctor.Coalgebra.isoMk._auto_1),
  (CategoryTheory.Endofunctor.Coalgebra.isoMk h w).inv.f = h.inv
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderiv_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (c : F), fderiv 𝕜 (Function.const E c) = 0
-- Mathlib.Util.Superscript
/-- Formatter for the superscript parser.  -/
Mathlib.Tactic.superscript.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Interval.Finset.Box
Finset.box_succ_union_prod : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : LocallyFiniteOrder α]
  [inst_4 : DecidableEq α] (n : ℕ), Finset.box (n + 1) ∪ Finset.Icc (-↑n) ↑n = Finset.Icc (-↑n.succ) ↑n.succ
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot : Type
-- Std.Do.PostCond
/-- A postcondition expressing partial correctness.
That is, it expresses that *if* the asserted computation finishes without throwing an exception
*then* the result satisfies the given predicate `p`.
Nothing is asserted when the computation throws an exception.
 -/
Std.Do.PostCond.mayThrow : {α : Type u_1} → {ps : Std.Do.PostShape} → (α → Std.Do.Assertion ps) → Std.Do.PostCond α ps
-- Mathlib.Init
/-- Define a set of linters that are used in the `nightly-testing` branch
to catch any regressions.
 -/
linter.nightlyRegressionSet : Lean.Option Bool
-- Mathlib.Data.Fintype.Inv
Fintype.bijective_bijInv : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {f : α → β} (f_bij : Function.Bijective f),
  Function.Bijective (Fintype.bijInv f_bij)
-- Mathlib.Algebra.GroupWithZero.Regular
/-- In a non-trivial ring, the element `0` is not right-regular -- with typeclasses.  -/
not_isRightRegular_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] [nR : Nontrivial R], ¬IsRightRegular 0
-- Mathlib.Topology.MetricSpace.Defs
/-- Build a new metric space from an old one where the bundled bornology structure is provably
(but typically non-definitionaly) equal to some given bornology structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
 -/
MetricSpace.replaceBornology : {α : Type u_3} →
  [B : Bornology α] →
    (m : MetricSpace α) → (∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) → MetricSpace α
-- Init.WF
WellFounded.Nat.fix.go : {α : Sort u} →
  {motive : α → Sort v} →
    (h : α → ℕ) →
      ((x : α) → ((y : α) → InvImage (fun x1 x2 => x1 < x2) h y x → motive y) → motive x) →
        (fuel : ℕ) → (x : α) → h x < fuel → motive x
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorRight_mapComp_inv_toNatTrans_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {a b c : CategoryTheory.Cat} (F : a ⟶ b) (G : b ⟶ c)
  (X : CategoryTheory.Join C ↑a),
  ((CategoryTheory.Join.pseudofunctorRight C).mapComp F G).inv.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Join.mapPairComp (CategoryTheory.Functor.id C) F.toFunctor (CategoryTheory.Functor.id C)
              G.toFunctor).inv.app
        X)
      (match X with
      | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x)
      | CategoryTheory.Join.right x =>
        CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right (G.toFunctor.obj (F.toFunctor.obj x))))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldlM.eq_def : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (init : δ) (x : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.foldlM f init x =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => pure init
    | Std.DTreeMap.Internal.Impl.inner size k v l r => do
      let left ← Std.DTreeMap.Internal.Impl.foldlM f init l
      let middle ← f left k v
      Std.DTreeMap.Internal.Impl.foldlM f middle r
-- Aesop.Tree.Data
Aesop.NormalizationState.provenByNormalization : Lean.Meta.SavedState → Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep)) → Aesop.NormalizationState
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.processConstructor.match_1.splitter : (motive : List Lean.Name × List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u_1) →
  (x : List Lean.Name × List Lean.Elab.Tactic.RCases.RCasesPatt) →
    ((ns : List Lean.Name) → (tl : List Lean.Elab.Tactic.RCases.RCasesPatt) → motive (ns, tl)) → motive x
-- Mathlib.Order.Interval.Finset.Defs
WithTop.instLocallyFiniteOrder : (α : Type u_1) → [inst : PartialOrder α] → [OrderTop α] → [LocallyFiniteOrder α] → LocallyFiniteOrder (WithTop α)
-- Mathlib.Algebra.Order.Invertible
invOf_lt_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} [inst_3 : Invertible a],
  ⅟a < 0 ↔ a < 0
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.termSum_one : ∀ (N : ℕ), ZetaAsymptotics.termSum 1 N = Real.log (↑N + 1) - ↑(harmonic (N + 1)) + 1
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.liftOn_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {α : Type u_2} (m : M) (s : ℕ+) (f : M → ℕ+ → α)
  (h : ∀ (m m' : M) (s s' : ℕ+), DivisibleHull.mk m s = DivisibleHull.mk m' s' → f m s = f m' s'),
  (DivisibleHull.mk m s).liftOn f h = f m s
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.instArchimedean : Archimedean ℝ
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.degree_derivative_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, (Polynomial.derivative p).degree ≤ p.degree
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroupOp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  Topology.IsQuotientMap f →
    ∀ [inst_2 : AddGroup E] [IsTopologicalAddGroup E] (G : AddSubgroup E),
      IsDiscrete ↑G → (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ -e₁ + e₂ ∈ G) → IsAddQuotientCoveringMap f ↥G.op
-- Init.Data.String.Iterate
String.Slice.instInhabitedByteIterator : Inhabited String.Slice.ByteIterator
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.all.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionHomLeft`, the action of `D` on morphisms in `C`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.«term_⊵ᵣ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.IsMittagLeffler.eq_image_eventualRange : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j : J}
  [CategoryTheory.IsCofilteredOrEmpty J],
  F.IsMittagLeffler →
    ∀ (f : j ⟶ i), F.eventualRange i = ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) '' F.eventualRange j
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_add_sphere : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E), {x} + Metric.sphere y δ = Metric.sphere (x + y) δ
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.whiskeringLeft_preservesLimitsOfShape : ∀ {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] (J : Type u) [inst_3 : CategoryTheory.Category.{v, u} J]
  [CategoryTheory.Limits.HasLimitsOfShape J D] (F : CategoryTheory.Functor C E),
  CategoryTheory.Limits.PreservesLimitsOfShape J ((CategoryTheory.Functor.whiskeringLeft C E D).obj F)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.elim_infty : ∀ {X : Type u_1} {Y : Type u_2} (y : Y) (f : X → Y), OnePoint.infty.elim y f = y
-- Init.Data.String.Bootstrap
String.Internal.any : String → (Char → Bool) → Bool
-- Mathlib.Order.Partition.Basic
Partition.pairwiseDisjoint : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] {P : Partition s}, (↑P).PairwiseDisjoint id
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.sigmaMap_apply : ∀ {α : Type u_1} {α' : Type u_2} {β : α → Type u_3} {β' : α' → Type u_4} (f : α ↪ α') (g : (a : α) → β a ↪ β' (f a))
  (x : (a : α) × β a), (f.sigmaMap g) x = Sigma.map (⇑f) (fun a => ⇑(g a)) x
-- Std.Time.Zoned.RecurringRule
/-- `Mm.w.d` form: month `m`, week `w` (1–5; 5 = last), ISO weekday `d`.
 -/
Std.Time.TimeZone.TransitionSpec.mwd : Std.Time.Month.Ordinal → Std.Time.Week.Aligned.Ordinal → Std.Time.Weekday.Ordinal → Std.Time.TimeZone.TransitionSpec
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_lt_self_iff : ∀ {a b : ENNReal}, a ≠ ⊤ → (a - b < a ↔ 0 < a ∧ 0 < b)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.stx.injEq : ∀ (id : Lean.Name) (ref : Lean.Syntax) (id_1 : Lean.Name) (ref_1 : Lean.Syntax),
  (Lean.Meta.Origin.stx id ref = Lean.Meta.Origin.stx id_1 ref_1) = (id = id_1 ∧ ref = ref_1)
-- Mathlib.RingTheory.NormalClosure
Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S],
  IsIntegralClosure (Ring.NormalClosure R S) S
    ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.dotProduct_adjMatrix : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (v : V) (vec : V → α),
  vec ⬝ᵥ SimpleGraph.adjMatrix α G v = ∑ u ∈ G.neighborFinset v, vec u
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInfo.mk.injEq : ∀ (all : Array Lean.Name) (numNested : ℕ) (all_1 : Array Lean.Name) (numNested_1 : ℕ),
  ({ all := all, numNested := numNested } = { all := all_1, numNested := numNested_1 }) =
    (all = all_1 ∧ numNested = numNested_1)
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.ind_iff_ind_underMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {X Y : C} (f : X ⟶ Y),
  P.ind f ↔ P.underObj.ind (CategoryTheory.Under.mk f)
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
/-- Given `sq' : SqStruct c p f g j`, this is the commutative square
```
               sq'.f'
F.obj j --------------------> X
   |                          |
   |                          |p
   v                      g   v
F.obj (succ j) ---> c.pt ---> Y
```

(Using the lifting property for this square is the key ingredient
in the proof that the left lifting property with respect to `p`
is stable under transfinite composition.)  -/
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.sq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (sq' : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j)
  [inst_3 : SuccOrder J],
  CategoryTheory.CommSq sq'.f' (F.map (CategoryTheory.homOfLE ⋯)) p
    (CategoryTheory.CategoryStruct.comp (c.ι.app (Order.succ j)) g)
-- Init.Data.FloatArray.Basic
FloatArray.instInhabited : Inhabited FloatArray
-- Mathlib.SetTheory.Ordinal.FixedPoint
/-- The fixed point lemma for normal functions: any normal function has an unbounded set of
fixed points.  -/
Ordinal.not_bddAbove_fp : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ¬BddAbove (Function.fixedPoints f)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.unsat_eq_certC.eq_1 : ∀ (p : Lean.Grind.CommRing.Poly) (k : ℤ) (c : ℕ),
  Lean.Grind.CommRing.Stepwise.unsat_eq_certC p k c = (!(k % ↑c).beq' 0).and' (p.beq' (Lean.Grind.CommRing.Poly.num k))
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.instCategory.eq_1 : Semigrp.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := MulHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @Semigrp.instCategory._proof_1,
    comp_id := @Semigrp.instCategory._proof_2, assoc := @Semigrp.instCategory._proof_3 }
-- Mathlib.Topology.Algebra.Group.Basic
/-- A monoid homomorphism (a bundled morphism of a type that implements `MonoidHomClass`) from a
topological group to a topological monoid is continuous provided that it is continuous at one. See
also `uniformContinuous_of_continuousAt_one`.  -/
continuous_of_continuousAt_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {M : Type u_1} {hom : Type u_2}
  [inst_3 : MulOneClass M] [inst_4 : TopologicalSpace M] [ContinuousMul M] [inst_6 : FunLike hom G M]
  [MonoidHomClass hom G M] (f : hom), ContinuousAt (⇑f) 1 → Continuous ⇑f
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.lift_eq_omega_ofNat : ∀ {o : Ordinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Ordinal.lift.{v, u} o = Ordinal.omega (OfNat.ofNat n) ↔ o = Ordinal.omega (OfNat.ofNat n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_erase_eq_of_not_compare_maxKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k fallback : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    ¬compare k (t.maxKeyD fallback) = Ordering.eq →
      (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Only assumes left strict covariance.  -/
Left.mul_lt_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftStrictMono α] [MulRightMono α] {a b c d : α},
  a < b → c < d → a * c < b * d
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.LeftUnitorBimod.hom_inv_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S),
  CategoryTheory.CategoryStruct.comp (Bimod.LeftUnitorBimod.hom P) (Bimod.LeftUnitorBimod.inv P) =
    CategoryTheory.CategoryStruct.id (Bimod.TensorBimod.X (Bimod.regular R) P)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous at a point
`x₀ : X` within a subset `S : Set X` iff the family `𝓕'`, obtained by composing each function
of `𝓕` by `u`, is equicontinuous at `x₀` within `S`.  -/
IsUniformInducing.equicontinuousWithinAt_iff : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} {β : Type u_8} [tX : TopologicalSpace X] [uα : UniformSpace α]
  [uβ : UniformSpace β] {F : ι → X → α} {S : Set X} {x₀ : X} {u : α → β},
  IsUniformInducing u → (EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x => u ∘ x) ∘ F) S x₀)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- A base angle of an isosceles triangle is acute, oriented angle-at-point form.  -/
EuclideanGeometry.abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, dist p₁ p₂ = dist p₁ p₃ → |(EuclideanGeometry.oangle p₂ p₃ p₁).toReal| < Real.pi / 2
-- Mathlib.Logic.Hydra
Relation.cutExpand_iff : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableEq α] [Std.Irrefl r] {s' s : Multiset α},
  Relation.CutExpand r s' s ↔ ∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.measure_pos_of_mem_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  {s : Set X} {x : X}, s ∈ nhds x → 0 < μ s
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.mapNeighborSet_apply_coe : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V) (w : ↑(G.neighborSet v)),
  ↑((f.mapNeighborSet v) w) = f ↑w
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_injective : ∀ {R : Type u_1} [inst : Semiring R], Function.Injective ⇑SkewPolynomial.C
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.ProductiveRel : (α₁ α₂ : Type w) →
  (m : Type w → Type w') →
    (β : Type w) →
      [Monad m] →
        [inst : Std.Iterator α₁ m β] →
          [inst_1 : Std.Iterator α₂ m β] →
            [Std.Iterators.Productive α₁ m] → [Std.Iterators.Productive α₂ m] → Std.IterM m β → Std.IterM m β → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSpace.comap_indicator_const_le_generateFrom_singleton : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : MeasurableSpace M] (s : Set α) (c : M),
  MeasurableSpace.comap (s.indicator fun x => c) inferInstance ≤ MeasurableSpace.generateFrom {s}
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- the chain complex involved in the resolution  -/
CategoryTheory.ProjectiveResolution.complex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} → CategoryTheory.ProjectiveResolution Z → ChainComplex C ℕ
-- Mathlib.Tactic.MkIffOfInductiveProp
Mathlib.Tactic.MkIff.Shape.mk.injEq : ∀ (variablesKept : List Bool) (neqs : Option ℕ) (variablesKept_1 : List Bool) (neqs_1 : Option ℕ),
  ({ variablesKept := variablesKept, neqs := neqs } = { variablesKept := variablesKept_1, neqs := neqs_1 }) =
    (variablesKept = variablesKept_1 ∧ neqs = neqs_1)
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.fderiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (p : Polynomial 𝕜),
  fderiv 𝕜 (fun x => Polynomial.eval x p) x =
    ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.collectHeaders : {α : Type} → StateT (ℕ × String) Lean.MetaM α → Lean.MetaM (α × String)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_eq_lsub' : ∀ {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (f : ι → Ordinal.{max u v}),
  (Ordinal.type r).blsub (Ordinal.bfamilyOfFamily' r f) = Ordinal.lsub f
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.instOneId.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {A : Type u_4} [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A],
  MulDistribMulActionHom.instOneId = { one := MulDistribMulActionHom.id M }
-- Mathlib.Analysis.Distribution.TestFunction
/-- **Alias** of `FunLike.coeAddMonoidHom_apply`. -/
TestFunction.coeFnAddMonoidHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β] (f : F), (FunLike.coeAddMonoidHom F α β) f = ⇑f
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion.group`.

---

Torsion monoids are really groups.  -/
IsTorsion.group : {G : Type u_1} → [inst : Monoid G] → IsMulTorsion G → Group G
-- Mathlib.Data.List.Sublists
List.subperm_of_sublists'_subperm_sublists' : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.sublists'.Subperm l₂.sublists' → l₁.Subperm l₂
-- Aesop.ElabM
Aesop.ElabM.Context.mk : Bool → Lean.MVarId → Aesop.ElabM.Context
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_snd_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme}
  (h : I.subscheme ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.comapIso f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f I.subschemeι) h) =
    CategoryTheory.CategoryStruct.comp ((I.comap f).subschemeMap I f ⋯) h
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of a Dirichlet character mod `N > 0` does not converge absolutely at `s = 1`.  -/
DirichletCharacter.not_LSeriesSummable_at_one : ∀ {N : ℕ}, N ≠ 0 → ∀ (χ : DirichletCharacter ℂ N), ¬LSeriesSummable (fun n => χ ↑n) 1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_injective_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Surjective ⇑f → Function.Injective (AddSubsemigroup.comap f)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (v_3 : V) (h : G.Adj u v_3) (p : G.Walk v_3 v),
  (SimpleGraph.Walk.cons h p).getVert 0 = u
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- If `X` is Galois, then the action of `Aut X` on `F.obj X` is
transitive for every fiber functor `F`.  -/
CategoryTheory.PreGaloisCategory.isPretransitive_of_isGalois : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  [CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive (CategoryTheory.Aut X) (F.obj X).obj
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.ofList_equiv_foldl : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α},
  (Std.HashSet.Raw.ofList l).Equiv (List.foldl (fun acc a => acc.insert a) ∅ l)
-- Init.Data.String.Basic
String.ofList_injective : ∀ {l₁ l₂ : List Char}, String.ofList l₁ = String.ofList l₂ → l₁ = l₂
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects : (S : Type u_1) →
  [inst : AddMonoidWithOne S] →
    (C : Type (u + 1)) →
      [inst_1 : CategoryTheory.LargeCategory C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          {FC : C → C → Type u_2} →
            {CC : C → Type u_3} →
              [inst_3 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
                [inst_4 : CategoryTheory.ConcreteCategory C FC] →
                  [inst_5 : CategoryTheory.HasShift C S] →
                    CategoryTheory.ConcreteCategory (CategoryTheory.DifferentialObject S C)
                      (CategoryTheory.DifferentialObject.HomSubtype S C)
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_sup : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (C D : PointedCone R M), PointedCone.dual p ↑(C ⊔ D) = PointedCone.dual p (↑C ∪ ↑D)
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_nonempty_iff : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} {P : Finpartition a}, P.parts.Nonempty ↔ a ≠ ⊥
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_right_hasFDerivAt_iff' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E} {f' : E →L[𝕜] G},
  HasFDerivAt (f ∘ ⇑iso) f' x ↔ HasFDerivAt f (f' ∘SL ↑iso.symm) (iso x)
-- Init.Data.UInt.Lemmas
UInt8.toNat_toUInt32 : ∀ (x : UInt8), x.toUInt32.toNat = x.toNat