mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.symm_p : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasBinaryProducts C],
  P.symm.p = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.Limits.prod.braiding A A).hom
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.term_zero : ∀ (f : ℕ → ℂ) (s : ℂ), LSeries.term f s 0 = 0
-- Mathlib.Data.Quot
true_equivalence : ∀ {α : Sort u_1}, Equivalence fun x x_1 => True
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.comp_neg_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) {Z : C} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (-g) h) =
    CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp f g) h
-- Lean.Parser.Do
Lean.Parser.Term.doMatch.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- The `n`-cycles `Zₙ(G, A)` of a `k`-linear `G`-representation `A`, i.e. the kernel of the
differential `Cₙ(G, A) ⟶ Cₙ₋₁(G, A)` in the complex of inhomogeneous chains.  -/
groupHomology.cycles : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ℕ → ModuleCat k
-- Mathlib.Computability.TuringDegree
/-- If a function is partial recursive, then it is recursive in every partial function.  -/
Partrec.turingReducible : ∀ {f g : ℕ →. ℕ}, Partrec f → TuringReducible f g
-- Mathlib.Logic.Basic
beq_eq_beq : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [LawfulBEq α] [inst_2 : BEq β] [LawfulBEq β] {a₁ a₂ : α} {b₁ b₂ : β},
  (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)}
  (φ : X ⟶ Y),
  (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₃ =
    CategoryTheory.Arrow.Hom.left (CategoryTheory.Arrow.Hom.right φ)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Multiplying the second vector passed to `oangle` by a negative real produces the same angle
as negating that vector.  -/
Orientation.oangle_smul_right_of_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ}, r < 0 → o.oangle x (r • y) = o.oangle x (-y)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.inv : ∀ {α : Type u_2} {f : Equiv.Perm α}, f.IsCycle → f⁻¹.IsCycle
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.instIsRightAdjointOfReflective : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (i : CategoryTheory.Functor D C) [CategoryTheory.Reflective i], i.IsRightAdjoint
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
LieAddGroup.of_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {m n : WithTop ℕ∞},
  m ≤ n → ∀ [h : LieAddGroup I n G], LieAddGroup I m G
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_neg : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] [inst_1 : HasDistribNeg α] (w : m → α) (v : n → α),
  Matrix.vecMulVec w (-v) = -Matrix.vecMulVec w v
-- Batteries.Tactic.PrintPrefix
Batteries.Tactic.PrintPrefixConfig.mk.sizeOf_spec : ∀ (imported propositions propositionsOnly showTypes internals : Bool),
  sizeOf
      { imported := imported, propositions := propositions, propositionsOnly := propositionsOnly,
        showTypes := showTypes, internals := internals } =
    1 + sizeOf imported + sizeOf propositions + sizeOf propositionsOnly + sizeOf showTypes + sizeOf internals
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.preimage_opensRange : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  (TopologicalSpace.Opens.map f.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f) = ⊤
-- Mathlib.Topology.Algebra.ConstMulAction
IsClosed.smul_of_ne_zero : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {c : G₀} {s : Set α}, IsClosed s → c ≠ 0 → IsClosed (c • s)
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.associated_generator_span_self : ∀ {R : Type u} [inst : CommSemiring R] [IsDomain R] (r : R),
  Associated (Submodule.IsPrincipal.generator (Ideal.span {r})) r
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicator_subset : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) {E₁ E₂ : Set α},
  E₁ ⊆ E₂ → ⇑(thickenedIndicator δ_pos E₁) ≤ ⇑(thickenedIndicator δ_pos E₂)
-- Mathlib.Order.Circular.ZMod
Int.btw_iff : ∀ {a b c : ℤ}, btw a b c ↔ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b
-- Mathlib.NumberTheory.NumberField.ProductFormula
/-- For any non-zero `x` in `𝓞 K`, the product of `w x`, where `w` runs over `FinitePlace K`, is
equal to the inverse of the absolute value of `Algebra.norm ℤ x`.  -/
NumberField.FinitePlace.prod_eq_inv_abs_norm_int : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.RingOfIntegers K},
  x ≠ 0 → ∏ᶠ (w : NumberField.FinitePlace K), w ↑x = |↑((Algebra.norm ℤ) x)|⁻¹
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.Subcanonical.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C},
  J ≤ CategoryTheory.Sheaf.canonicalTopology C → J.Subcanonical
-- Mathlib.Analysis.Convex.Function
strictConcaveOn_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [inst_6 : SMul 𝕜 E]
  [inst_7 : SMul 𝕜 β] {s : Set E} {f : E → β},
  StrictConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄,
            y ∈ s →
              x ≠ y →
                ∀ ⦃a b : 𝕜⦄,
                  0 < a → 0 < b → (a / (a + b)) • f x + (b / (a + b)) • f y < f ((a / (a + b)) • x + (b / (a + b)) • y)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get.congr_simp : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m m_1 : Std.DHashMap.Raw α fun x => β) (e_m : m = m_1)
  (a a_1 : α) (e_a : a = a_1) (h : a ∈ m), Std.DHashMap.Raw.Const.get m a h = Std.DHashMap.Raw.Const.get m_1 a_1 ⋯
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.Semigrp.Hom.mk : {A B : Semigrp} → (↑A →ₙ* ↑B) → A.Hom B
-- Mathlib.RingTheory.Extension.Basic
/-- The ring `T ⊗[R] P.Ring` underlying the extension `P.baseChange T` is a `P.Ring`-algebra
by action on the right. This causes a (mathematical) diamond when `T = P.Ring`, so it is
not an instance.
 -/
Algebra.Extension.algebraBaseChange : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (P : Algebra.Extension R S) →
            (T : Type u_1) → [inst_3 : CommRing T] → [inst_4 : Algebra R T] → Algebra P.Ring P.baseChange.Ring
-- Mathlib.Data.Set.Basic
Set.inter_congr_right : ∀ {α : Type u} {s t u : Set α}, t ∩ u ⊆ s → s ∩ u ⊆ t → s ∩ u = t ∩ u
-- Mathlib.Analysis.Polynomial.Basic
/-- **Alias** of `Polynomial.div_tendsto_atTop_leadingCoeff_div_of_degree_eq`. -/
Polynomial.div_tendsto_leadingCoeff_div_of_degree_eq : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  P.degree = Q.degree →
    Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop
      (nhds (P.leadingCoeff / Q.leadingCoeff))
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.instAlgebraZModExtension : (k : Type u_1) →
  [inst : Field k] →
    (p : ℕ) →
      [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP k p] → (n : ℕ) → Algebra (ZMod p) (FiniteField.Extension k p n)
-- Mathlib.Order.Cover
Set.OrdConnected.apply_covBy_apply_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} (f : α ↪o β),
  (Set.range ⇑f).OrdConnected → (f a ⋖ f b ↔ a ⋖ b)
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {K : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} K] (e : J ≌ K) {F : CategoryTheory.Functor K C}
  {c : CategoryTheory.Limits.Cocone F},
  CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.Cocone.whisker e.functor c) ↔
    CategoryTheory.IsVanKampenColimit c
-- Mathlib.Data.Finset.Sort
StrictMonoOn.map_finsetSort : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) [inst : LinearOrder α] [inst_1 : LinearOrder β],
  StrictMonoOn ⇑f ↑s → List.map (⇑f) (s.sort fun a b => a ≤ b) = (Finset.map f s).sort fun a b => a ≤ b
-- Init.Grind.Order
Lean.Grind.Order.lt_of_not_le : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsLinearPreorder α] {a b : α}, ¬a ≤ b → b < a
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.algHom_ext : ∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (A i)] [inst_2 : (i : ι) → Module R (A i)] [inst_3 : AddMonoid ι]
  [inst_4 : DirectSum.GSemiring A] [inst_5 : Semiring B] [inst_6 : DirectSum.GAlgebra R A] [inst_7 : Algebra R B]
  [inst_8 : DecidableEq ι] ⦃f g : (DirectSum ι fun i => A i) →ₐ[R] B⦄,
  (∀ (i : ι) (x : A i), f ((DirectSum.of A i) x) = g ((DirectSum.of A i) x)) → f = g
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.evaluation₄_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  CategoryTheory.Square.evaluation₄.obj sq = sq.X₄
-- Mathlib.Data.TypeVec
/-- n-tuples of types, as a category  -/
TypeVec : ℕ → Type (u_1 + 1)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
SeparationQuotient.instCompleteSpace : ∀ {α : Type u} [inst : UniformSpace α] [CompleteSpace α], CompleteSpace (SeparationQuotient α)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.universallyInjective_eq : @AlgebraicGeometry.UniversallyInjective =
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x =>
      Function.Injective x).universally
-- Mathlib.GroupTheory.Sylow
/-- A Sylow `p`-subgroup is a maximal `p`-subgroup.  -/
Sylow : ℕ → (G : Type u_1) → [Group G] → Type u_1
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.toList_flatMapAfterM : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α Id]
  [Std.Iterators.Finite α₂ m] {f : β → m (Std.IterM m γ)} {it₁ : Std.Iter β} {it₂ : Option (Std.IterM m γ)},
  (Std.Iter.flatMapAfterM f it₁ it₂).toList =
    match it₂ with
    | none =>
      List.flatten <$>
        (Std.Iter.mapM
            (fun b => do
              let __do_lift ← f b
              __do_lift.toList)
            it₁).toList
    | some it₂ => do
      let __do_lift ← it₂.toList
      let __do_lift_1 ←
        List.flatten <$>
            (Std.Iter.mapM
                (fun b => do
                  let __do_lift ← f b
                  __do_lift.toList)
                it₁).toList
      pure (__do_lift ++ __do_lift_1)
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.isLocalizedEquivalence_of_isInduced : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence]
  [Φ.IsInduced] [W₂.RespectsIso], Φ.IsLocalizedEquivalence
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Let `s : Set 𝕜` be a compact set and consider pairs `(f, a) : (𝕜 → 𝕜) × A` where `f` is
continuous on `s`, maps zero itself, and `quasispectrum 𝕜 a ⊆ s` and `a` satisfies the predicate
`p a` for the continuous functional calculus.

Then `cfcₙ` is jointly continuous in both variables (i.e., continuous in its uncurried form) on this
set of pairs when the function space is equipped with the topology of uniform convergence on `s`.  -/
continuousOn_cfcₙ_setProd : ∀ {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [ContinuousStar A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {s : Set 𝕜},
  IsCompact s →
    ContinuousOn (fun fa => cfcₙ ((UniformOnFun.toFun {s}) fa.1) fa.2)
      ({f | ContinuousOn ((UniformOnFun.toFun {s}) f) s ∧ f 0 = 0} ×ˢ {a | p a ∧ quasispectrum 𝕜 a ⊆ s})
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} [hi : Inhabited β] {f : β → β},
      (t.modify k f)[k']! = if cmp k k' = Ordering.eq then (Option.map f t[k]?).get! else t[k']!
-- Mathlib.Geometry.Euclidean.PerpBisector
/-- Suppose that `c₁` is equidistant from `p₁` and `p₂`, and the same applies to `c₂`. Then the
vector between `c₁` and `c₂` is orthogonal to that between `p₁` and `p₂`. (In two dimensions, this
says that the diagonals of a kite are orthogonal.)  -/
EuclideanGeometry.inner_vsub_vsub_of_dist_eq_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] {c₁ c₂ p₁ p₂ : P},
  dist p₁ c₁ = dist p₂ c₁ → dist p₁ c₂ = dist p₂ c₂ → inner ℝ (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterMatrix.toCoxeterSystem_simple : ∀ {B : Type u_1} (M : CoxeterMatrix B), M.toCoxeterSystem.simple = M.simple
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_right : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] (d : D) {c c' : C}
  (f : c ⟶ c'),
  CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f))
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- `CuspFormClass F Γ k` says that `F` is a type of bundled functions that extend
`SlashInvariantFormClass` by requiring that the functions be holomorphic and zero
at all cusps.  -/
CuspFormClass : (F : Type u_2) → outParam (Subgroup (GL (Fin 2) ℝ)) → outParam ℤ → [FunLike F UpperHalfPlane ℂ] → Prop
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The `Subfield` generated by a set in a field.  -/
_private.Mathlib.Algebra.Field.Subfield.Basic.0.Subfield.commClosure : {K : Type u} → [inst : Field K] → Set K → Subfield K
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_add_natCast : ∀ (r : ENNReal) (n : ℕ), ⌈r + ↑n⌉ₑ = ⌈r⌉ₑ + ↑n
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanDidOpenTextDocumentParams.mk.injEq : ∀ (toDidOpenTextDocumentParams : Lean.Lsp.DidOpenTextDocumentParams)
  (dependencyBuildMode? : Option Lean.Lsp.DependencyBuildMode)
  (toDidOpenTextDocumentParams_1 : Lean.Lsp.DidOpenTextDocumentParams)
  (dependencyBuildMode?_1 : Option Lean.Lsp.DependencyBuildMode),
  ({ toDidOpenTextDocumentParams := toDidOpenTextDocumentParams, dependencyBuildMode? := dependencyBuildMode? } =
      { toDidOpenTextDocumentParams := toDidOpenTextDocumentParams_1,
        dependencyBuildMode? := dependencyBuildMode?_1 }) =
    (toDidOpenTextDocumentParams = toDidOpenTextDocumentParams_1 ∧ dependencyBuildMode? = dependencyBuildMode?_1)
-- Init.Control.Lawful.Basic
/-- An alternative constructor for `LawfulMonad` which has more
defaultable fields in the common case.
 -/
LawfulMonad.mk' : ∀ (m : Type u → Type v) [inst : Monad m],
  (∀ {α : Type u} (x : m α), id <$> x = x) →
    (∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x) →
      (∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) →
        autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <$> y)
            LawfulMonad.mk'._auto_1 →
          autoParam
              (∀ {α β : Type u} (x : m α) (y : m β),
                x <* y = do
                  let a ← x
                  let _ ← y
                  pure a)
              LawfulMonad.mk'._auto_3 →
            autoParam
                (∀ {α β : Type u} (x : m α) (y : m β),
                  x *> y = do
                    let _ ← x
                    y)
                LawfulMonad.mk'._auto_5 →
              autoParam
                  (∀ {α β : Type u} (f : α → β) (x : m α),
                    (do
                        let y ← x
                        pure (f y)) =
                      f <$> x)
                  LawfulMonad.mk'._auto_7 →
                autoParam
                    (∀ {α β : Type u} (f : m (α → β)) (x : m α),
                      (do
                          let x_1 ← f
                          x_1 <$> x) =
                        f <*> x)
                    LawfulMonad.mk'._auto_9 →
                  LawfulMonad m
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.map_mod : ∀ {n d : ℕ} (a : Fin n.succ → ℕ), (Behrend.map d) a % d = a 0 % d
-- Init.Data.SInt.Lemmas
Int8.lt_iff_toBitVec_slt : ∀ {a b : Int8}, a < b ↔ a.toBitVec.slt b.toBitVec = true
-- Mathlib.Data.NNReal.Defs
NNReal.coe_mul : ∀ (r₁ r₂ : NNReal), ↑(r₁ * r₂) = ↑r₁ * ↑r₂
-- Mathlib.Algebra.Ring.Prod
RingHom.fst_comp_prod : ∀ {R : Type u_1} {S : Type u_3} {T : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (f : R →+* S) (g : R →+* T), (RingHom.fst S T).comp (f.prod g) = f
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.nhds_bot_basis : (nhds ⊥).HasBasis (fun x => True) fun x => Set.Iio ↑x
-- Mathlib.FieldTheory.RatFunc.Luroth
RatFunc.Luroth.generator_ne_C : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → ¬∃ c, RatFunc.Luroth.generator E = RatFunc.C c
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_sub_natCast : ∀ (r : ENNReal) (n : ℕ), ⌊r - ↑n⌋ₑ = ⌊r⌋ₑ - ↑n
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_neg' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → E}, (μ.withDensityᵥ fun x => -f x) = -μ.withDensityᵥ f
-- Mathlib.Algebra.CharP.Defs
/-- The exponential characteristic is one iff the characteristic is zero.  -/
expChar_one_iff_char_zero : ∀ (R : Type u_1) [inst : NonAssocSemiring R] [Nontrivial R] (p q : ℕ) [CharP R p] [ExpChar R q], q = 1 ↔ p = 0
-- Mathlib.Data.Fin.Tuple.Basic
/-- If a predicate `q` holds at some `x` and implies `p` up to that `x`, then
the earliest `xq` such that `q xq` is at least the smallest `xp` where `p xp`.
The stronger version of `Fin.find_mono`, since this one needs
implication only up to `Fin.find _` while the other requires `q` implying `p` everywhere.  -/
Fin.find_mono_of_le : ∀ {n : ℕ} {p q : Fin n → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] {i : Fin n} (hi : q i)
  (hpq : ∀ j ≤ i, q j → p j), Fin.find p ⋯ ≤ Fin.find q ⋯
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.coe_inj : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {q r : ℚ}, ↑q = ↑r ↔ q = r
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Init.Data.Int.Linear
Int.Internal.Linear.natCast_sub : ∀ (x y : ℕ), ↑(x - y) = if ↑y + -1 * ↑x ≤ 0 then ↑x + -1 * ↑y else 0
-- Mathlib.Logic.Function.DependsOn
dependsOn_iff_factorsThrough : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} {s : Set ι},
  DependsOn f s ↔ Function.FactorsThrough f s.domRestrict
-- Mathlib.Algebra.Group.Hom.Instances
ZeroHom.instZSMul : {M : Type uM} → {N : Type uN} → [inst : Zero M] → [inst_1 : AddGroup N] → SMul ℤ (ZeroHom M N)
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.head_neg : ∀ {α : Type u_1} {n : ℕ} [inst : Neg α] (a : Fin n.succ → α), Matrix.vecHead (-a) = -Matrix.vecHead a
-- Mathlib.Data.PNat.Factors
/-- If a `Multiset ℕ+` consists only of primes, it can be recast as a `PrimeMultiset`.  -/
PrimeMultiset.ofPNatMultiset : (v : Multiset ℕ+) → (∀ p ∈ v, p.Prime) → PrimeMultiset
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_inter!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter! m₂).getKey! k = m₁.getKey! k