mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- Define a `Kernel (γ × α) β` from a `Kernel α β` by taking the comap of the projection.  -/
ProbabilityTheory.Kernel.prodMkLeft : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (γ : Type u_5) → [inst : MeasurableSpace γ] → ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel (γ × α) β
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_ringHom_inj_iff : ∀ {R : Type u_7} {S : Type u_8} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f g : R ≃+* S),
  f = g ↔ ↑f = ↑g
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
instRightCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsRightCancelMulZero : {M₀ : Type u_2} →
  [inst : MonoidWithZero M₀] → [Nontrivial M₀] → [IsRightCancelMulZero M₀] → RightCancelMonoid ↥(nonZeroDivisors M₀)
-- Mathlib.Tactic.CasesM
/-- `casesm p` searches for the first hypothesis `h : type` where `type` matches the term `p`,
and splits the main goal by cases on `h`. Use holes in `p` to indicate arbitrary subexpressions,
for example `casesm _ ∧ _` will match any conjunction. `casesm p` fails if no hypothesis type
matches `p`.

* `casesm p_1, ..., p_n` searches for a hypothesis `h : type` where `type` matches one or more of
  the given patterns `p_1`, ... `p_n`, and splits the main goal by cases on `h`.
* `casesm* p` repeatedly performs case splits until no more hypothesis type matches `p`.
  This is a more efficient and compact version of `· repeat casesm p`.
  It is more efficient because the pattern is compiled once.
* `casesm! p` and `casesm!* p` skip a hypothesis if the main goal would be replaced with two or more
  subgoals.

Example:
```
example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  casesm* _∨_, _∧_
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial
```
 -/
Mathlib.Tactic.casesm! : Lean.ParserDescr
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.Clause.maxLiteral_eq_some_of_mem : ∀ {l : ℕ} (c : Std.Sat.CNF.Clause ℕ), Std.Sat.CNF.Clause.Mem l c → ∃ maxLit, c.maxLiteral = some maxLit
-- Mathlib.Probability.Moments.MGFAnalytic
/-- For `t : ℝ` with `t ∈ interior (integrableExpSet X μ)`, the derivative of the function
`x ↦ μ[X ^ n * exp (x * X)]` at `t` is `μ[X ^ (n + 1) * exp (t * X)]`.  -/
ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ),
      HasDerivAt (fun t => ∫ (x : Ω), (fun ω => X ω ^ n * Real.exp (t * X ω)) x ∂μ)
        (∫ (x : Ω), (fun ω => X ω ^ (n + 1) * Real.exp (t * X ω)) x ∂μ) t
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
ENat.instDiscreteMeasurableSpace : DiscreteMeasurableSpace ℕ∞
-- Init.Grind.Module.Basic
Lean.Grind.NatModule.toAddCommMonoid : {M : Type u} → [self : Lean.Grind.NatModule M] → Lean.Grind.AddCommMonoid M
-- Mathlib.Data.Holor
Holor.instModule : {α : Type} → {ds : List ℕ} → [inst : Semiring α] → Module α (Holor α ds)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.singularPart_of_subset_compl_mutuallySingularSetSlice : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [inst : ProbabilityTheory.IsSFiniteKernel κ]
  [inst_1 : ProbabilityTheory.IsFiniteKernel η] {a : α} {s : Set γ},
  s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ → ((κ.singularPart η) a) s = 0
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.inv_eq_eval : ∀ {M : Type u_1} [inst : CommGroupWithZero M] {l : Mathlib.Tactic.FieldSimp.NF M} {x : M}, x = l.eval → x⁻¹ = l⁻¹.eval
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H) (ψ : H → G)
  (hφ : Function.RightInverse ψ ⇑φ) (a : H),
  (QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ).symm a = (QuotientAddGroup.mk ∘ ψ) a
-- Init.Control.Id
/-- The identity function on types, used primarily for its `Monad` instance.

The identity monad is useful together with monad transformers to construct monads for particular
purposes. Additionally, it can be used with `do`-notation in order to use control structures such as
local mutability, `for`-loops, and early returns in code that does not otherwise use monads.

Examples:
```lean example
def containsFive (xs : List Nat) : Bool := Id.run do
  for x in xs do
    if x == 5 then return true
  return false
```

```lean example
#eval containsFive [1, 3, 5, 7]
```
```output
true
```
 -/
Id : Type u → Type u
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.binaryProductLimitCone_cone_π_app_right : ∀ {R : Type u} [inst : Ring R] (M N : ModuleCat R),
  (M.binaryProductLimitCone N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } =
    ModuleCat.ofHom (LinearMap.snd R ↑M ↑N)
-- Lean.Data.Options
Lean.OptionDecls : Type
-- Mathlib.Data.Int.DivMod
Int.fdiv_fdiv_eq_fdiv_mul : ∀ (m : ℤ) {n k : ℤ}, 0 ≤ n → 0 ≤ k → (m.fdiv n).fdiv k = m.fdiv (n * k)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_pi_iff : ∀ {α : Type u_1} {δ : Type u_4} {X : δ → Type u_6} [inst : MeasurableSpace α] [inst_1 : (a : δ) → MeasurableSpace (X a)]
  {g : α → (a : δ) → X a}, Measurable g ↔ ∀ (a : δ), Measurable fun x => g x a
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.ρ_hom_inv : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X : CategoryTheory.FreeMonoidalCategory C}, CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.LinearAlgebra.Projection
/-- Given linear maps `φ` and `ψ` from complement submodules, `LinearMap.ofIsCompl` is
the induced linear map over the entire module.  -/
LinearMap.ofIsCompl : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          {F : Type u_3} →
            [inst_3 : AddCommGroup F] →
              [inst_4 : Module R F] → {p q : Submodule R E} → IsCompl p q → (↥p →ₗ[R] F) → (↥q →ₗ[R] F) → E →ₗ[R] F
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of a constant function is the constant.
 -/
meromorphicTrailingCoeffAt_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x e : 𝕜}, meromorphicTrailingCoeffAt (fun x => e) x = e
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects colimits, then `F.leftOp : Cᵒᵖ ⥤ D` reflects limits.  -/
CategoryTheory.Limits.reflectsLimitsOfSize_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp
-- Mathlib.Analysis.Complex.Exponential
/-- **Alias** of the reverse direction of `Real.one_lt_exp_iff`. -/
_private.Mathlib.Analysis.Complex.Exponential.0.Real.Bound.one_lt_exp_of_pos : ∀ {x : ℝ}, 0 < x → 1 < Real.exp x
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.matroid_Indep : ∀ {α : Type u_1} (M : IndepMatroid α) (a : Set α), M.matroid.Indep a = M.Indep a
-- Lean.Expr
Lean.Expr.lit.injEq : ∀ (a a_1 : Lean.Literal), (Lean.Expr.lit a = Lean.Expr.lit a_1) = (a = a_1)
-- Std.Time.Format.Basic
Std.Time.instReprFormatPart.repr : Std.Time.FormatPart → ℕ → Std.Format
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instOrderBot : {M : Type u_1} → [inst : CommMonoid M] → OrderBot (Associates M)
-- Mathlib.Topology.Separation.Regular
/-- If `a` is a point that does not belong to a closed set `s`, then `a` and `s` admit disjoint
neighborhoods.  -/
RegularSpace.regular : ∀ {X : Type u} {inst : TopologicalSpace X} [self : RegularSpace X] {s : Set X} {a : X},
  IsClosed s → a ∉ s → Disjoint (nhdsSet s) (nhds a)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.comm_comp_includeLeft : ∀ (R : Type uR) (A : Type uA) (B : Type uB) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B],
  (↑(Algebra.TensorProduct.comm R A B)).comp Algebra.TensorProduct.includeLeft = Algebra.TensorProduct.includeRight
-- Lean.Meta.AppBuilder
/-- Given `h : False`, returns an instance of type `e`.  -/
Lean.Meta.mkFalseElim : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.comp_squareLeft : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A'']
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B''] [inst_8 : CategoryTheory.Category.{v₉, u₉} C'']
  {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''}
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''),
  (ψ.comp ψ').squareLeft = ψ.squareLeft.vComp' ψ'.squareLeft
-- Lean.Server.RequestCancellation
Lean.Server.CancellableM.run : {α : Type} →
  Lean.Server.RequestCancellationToken → Lean.Server.CancellableM α → IO (Except Lean.Server.RequestCancellation α)
-- Init.Data.List.Range
List.tail_range : ∀ {n : ℕ}, (List.range n).tail = List.range' 1 (n - 1)
-- Mathlib.Data.WSeq.Relation
_private.Mathlib.Data.WSeq.Relation.0.Stream'.WSeq.LiftRelO.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option (α × Stream'.WSeq α) → Option (β × Stream'.WSeq β) → Sort u_3)
  (x : Option (α × Stream'.WSeq α)) (x_1 : Option (β × Stream'.WSeq β)) (h_1 : Unit → motive none none)
  (h_2 : (a : α) → (s : Stream'.WSeq α) → (b : β) → (t : Stream'.WSeq β) → motive (some (a, s)) (some (b, t)))
  (h_3 : (x : Option (α × Stream'.WSeq α)) → (x_2 : Option (β × Stream'.WSeq β)) → motive x x_2),
  (x = none → x_1 = none → False) →
    (∀ (a : α) (s : Stream'.WSeq α) (b : β) (t : Stream'.WSeq β), x = some (a, s) → x_1 = some (b, t) → False) →
      (match x, x_1 with
        | none, none => h_1 ()
        | some (a, s), some (b, t) => h_2 a s b t
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.id_apply : ∀ (R : CommSemiRingCat) (r : ↑R), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id R)) r = r
-- Mathlib.FieldTheory.RatFunc.Basic
/-- `K⟮X⟯` is isomorphic to the field of fractions of `K[X]`, as rings.

This is an auxiliary definition; `simp`-normal form is `IsLocalization.algEquiv`.
 -/
RatFunc.toFractionRingRingEquiv : (K : Type u) → [inst : CommRing K] → RatFunc K ≃+* FractionRing (Polynomial K)
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
/-- A Mayer-Vietoris square in a category `C` equipped with a Grothendieck
topology consists of a commutative square `f₁₂ ≫ f₂₄ = f₁₃ ≫ f₃₄` in `C`
such that `f₁₃` is a monomorphism and that the square becomes a
pushout square in the category of sheaves of sets.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) → [CategoryTheory.HasWeakSheafify J (Type v)] → Type (max u v)
-- Lean.ToExpr
Lean.instToExprProdOfToLevel : {α : Type u} → {β : Type v} → [Lean.ToLevel] → [Lean.ToLevel] → [Lean.ToExpr α] → [Lean.ToExpr β] → Lean.ToExpr (α × β)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).maxKey?.isSome = true
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.decomposeTensor_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (ℳ : ι → Submodule R M) (N : Type u_5) [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {i : ι},
  DirectSum.decomposeTensor ℳ N i = (LinearMap.rTensor N (ℳ i).subtype).range
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.codeBlock.closeFence : Lean.Doc.Parser.BlockCtxt → ℕ → ℕ → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLEMk.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B)
  [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g]
  (h : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g),
  CategoryTheory.Subobject.ofMkLEMk f g h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Subobject.mk f).ofLE (CategoryTheory.Subobject.mk g) h)
        (CategoryTheory.Subobject.underlyingIso g).hom)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
/-- Displacement is at most the integral of an upper estimate on the speed.

Let `f : ℝ → E` be a function which is continuous on a closed interval `[a, b]`
and is differentiable on the open interval `(a, b)`.
If `B t` is an integrable upper estimate on `‖f' t‖`, `a < t < b`,
then `‖f b - f a‖ ≤ ∫ t in a..b, B t`.
 -/
norm_sub_le_integral_of_norm_deriv_le_of_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {B : ℝ → ℝ},
  a ≤ b →
    ContinuousOn f (Set.Icc a b) →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → ‖deriv f t‖ ≤ B t) →
          IntervalIntegrable B MeasureTheory.volume a b → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.comap_span_top : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E),
  Submodule.span K ↑L = ⊤ → ∀ {e : F →ₗ[K] E}, ↑L ⊆ ↑e.range → Submodule.span K ↑(ZLattice.comap K L e) = ⊤
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulZeroOneClass α] [inst_4 : MulZeroOneClass β] [inst_5 : MulZeroOneClass γ] {g : β →*₀o γ}
  {f₁ f₂ : α →*₀o β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (curr : ℕ)
  (hcurr : curr ≤ len) (s : aig.RefVec curr) (input : aig.RefVec len)
  (f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [inst_3 : Std.Sat.AIG.RefVec.LawfulMapOperator α f]
  (idx : ℕ) (hidx : idx < curr),
  (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).vec.get idx ⋯ = (s.get idx hidx).cast ⋯
-- Mathlib.Data.List.Sigma
List.of_mem_dlookup : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)},
  b ∈ List.dlookup a l → ⟨a, b⟩ ∈ l
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_codiag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f f) (CategoryTheory.Limits.codiag Y) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag X) f
-- Mathlib.Order.Minimal
minimal_minimal : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α], Minimal (Minimal P) x ↔ Minimal P x
-- Mathlib.Order.Interval.Set.Disjoint
Set.Iic_disjoint_Ioc : ∀ {α : Type v} [inst : Preorder α] {a b c : α}, a ≤ b → Disjoint (Set.Iic a) (Set.Ioc b c)
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- Any element of the spectrum of a selfadjoint is real.  -/
IsSelfAdjoint.mem_spectrum_eq_re : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A}, IsSelfAdjoint a → ∀ {z : ℂ}, z ∈ spectrum ℂ a → z = ↑z.re
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.powerSeriesMk_card_restricted_eq_tprod : ∀ (R : Type u_1) [inst : TopologicalSpace R] [T2Space R] [inst_2 : CommSemiring R] [IsTopologicalSemiring R]
  (p : ℕ → Prop) [inst_4 : DecidablePred p],
  (PowerSeries.mk fun n => ↑(Nat.Partition.restricted n p).card) =
    ∏' (i : ℕ), if p (i + 1) then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `Relation.SymmGen.of_lt`. -/
LT.lt.symmGen : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], a < b → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.ofClass.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (F : Type u_7) [inst_4 : FunLike F A B] [inst_5 : ContinuousMapClass F A B]
  [inst_6 : MonoidHomClass F A B] (f : F), ContinuousMonoidHom.ofClass A B F f = ↑f
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.DocM.exec.binderNames : Lean.Syntax → Lean.Elab.TermElabM (Array (Option Lean.Syntax))
-- Init.Data.Iterators.Basic
Std.IterStep.mapIterator_skip : ∀ {α : Type u} {β : Type w} {α' : Type u'} {f : α → α'} {it : α},
  Std.IterStep.mapIterator f (Std.IterStep.skip it) = Std.IterStep.skip (f it)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Prepend a monomial to a multiseries.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    ℝ →
      Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
          Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl
-- Mathlib.Data.Fin.Tuple.Embedding
Fin.Embedding.snoc_castSucc : ∀ {α : Type u_1} {n : ℕ} {x : Fin n ↪ α} {a : α} {ha : a ∉ Set.range ⇑x} {i : Fin n},
  (Fin.Embedding.snoc x ha) i.castSucc = x i
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.PlausibleStep.yieldNone : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} [inst : Std.Iterator α m β] {it : Std.IterM n γ}
  {it' : Std.IterM m β} {out : β},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    (f out).Property none →
      Std.Iterators.Types.FilterMap.PlausibleStep it
        (Std.IterStep.skip (Std.IterM.InternalCombinators.filterMap lift f it'))
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_prod : ∀ (α : Type u_3) (β : Type u_4), Nat.card (α × β) = Nat.card α * Nat.card β
-- Init.Data.List.Lex
List.IsPrefix.le : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2] {l₁ l₂ : List α}, l₁ <+: l₂ → l₁ ≤ l₂
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.abs_mulExpNegMulSq_one_le_one : ∀ (x : ℝ), |Real.mulExpNegMulSq 1 x| ≤ 1
-- Mathlib.Topology.Convenient.HomSpace
/-- Given a `X`-continuous map `p : Z → T`, this is the postcomposition with `p`
`ContinuousMapGeneratedBy X Y Z → ContinuousMapGeneratedBy X Y T`
as a `X`-continuous map.  -/
Topology.ContinuousMapGeneratedBy.postcomp : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} →
        [inst_1 : TopologicalSpace Y] →
          {Z : Type v'} →
            [inst_2 : TopologicalSpace Z] →
              {T : Type v''} →
                [inst_3 : TopologicalSpace T] →
                  [∀ (i : ι), LocallyCompactSpace (X i)] →
                    [∀ (i j : ι), Topology.IsGeneratedBy X (X i × X j)] →
                      Topology.ContinuousMapGeneratedBy X Z T →
                        Topology.ContinuousMapGeneratedBy X (Topology.ContinuousMapGeneratedBy X Y Z)
                          (Topology.ContinuousMapGeneratedBy X Y T)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalCommSemiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemigroup M],
  MonoidAlgebra.nonUnitalCommSemiring = { toNonUnitalSemiring := MonoidAlgebra.nonUnitalSemiring, mul_comm := ⋯ }
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.galgebra_toFun_def : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r : R),
  DirectSum.GAlgebra.toFun r = TensorPower.algebraMap₀ r
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.getParamRevDeps : Lean.Expr → Lean.MetaM (Array (Array ℕ))
-- Init.Data.Int.DivMod.Lemmas
Int.neg_ediv_self : ∀ (a : ℤ), a ≠ 0 → -a / a = -1
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.Hom.ext_iff : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v, u₂} D} {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} {x y : X.Hom Y}, x = y ↔ x.hom = y.hom
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₂.val_eq_coe : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : ↥(groupCohomology.cocycles₂ A)),
  ↑f = ⇑f
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- The quotient functor associated to a quotient category defines a natural map from the free
category on the underlying quiver of a refl quiver to the free category on the reflexive quiver.  -/
CategoryTheory.Cat.FreeRefl.quotientFunctor : (V : Type u_1) →
  [inst : CategoryTheory.ReflQuiver V] → CategoryTheory.Functor (CategoryTheory.Paths V) (CategoryTheory.Cat.FreeRefl V)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_eq_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp a b = toIocDiv hp 0 (b - a)
-- Mathlib.Logic.Relation
Std.Symm.map : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Std.Symm r] (f : α → β), Std.Symm (Relation.Map r f f)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
/-- A cycle `s : Cycle α`, given `Nodup s` can be interpreted as an `Equiv.Perm α`
where each element in the list is permuted to the next one, defined as `formPerm`.
 -/
Equiv.Perm.«termC[_,]» : Lean.ParserDescr
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sum_ground : ∀ {α : Type u} {β : Type v} (M : Matroid α) (N : Matroid β), (M.sum N).E = Sum.inl '' M.E ∪ Sum.inr '' N.E
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_iInf₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → LowerSet α),
  (⨅ i, ⨅ j, f i j).compl = ⨅ i, ⨅ j, (f i j).compl