mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.foldlM_toArray : ∀ {m : Type w → Type u_1} {γ α β : Type w} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.IterM Id β}
  {f : γ → β → m γ} {init : γ}, Array.foldlM f init it.toArray.run = Std.IterM.foldM f init it
-- Mathlib.CategoryTheory.Localization.HasLocalization
CategoryTheory.MorphismProperty.HasLocalization.hL : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.HasLocalization], CategoryTheory.MorphismProperty.HasLocalization.L.IsLocalization W
-- Mathlib.Data.Semiquot
Semiquot.pure_inj : ∀ {α : Type u_1} {a b : α}, pure a = pure b ↔ a = b
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.pushoutComp_hom_app_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : P.IsStableUnderCobaseChangeAlong f]
  [inst_3 : P.IsStableUnderCobaseChangeAlong g] [inst_4 : P.HasPushoutsAlong f] [inst_5 : P.HasPushoutsAlong g]
  [inst_6 : Q.RespectsIso] [inst_7 : Q.IsStableUnderCobaseChange]
  (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g))
  (hfg :
    autoParam (fg = CategoryTheory.CategoryStruct.comp f g) CategoryTheory.MorphismProperty.Under.pushoutComp._auto_1)
  (X_1 : P.Under Q X),
  ((CategoryTheory.MorphismProperty.Under.pushoutComp f g fg hfg).hom.app X_1).right =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.map X_1.hom fg X_1.hom (CategoryTheory.CategoryStruct.comp f g)
        (CategoryTheory.CategoryStruct.id X_1.right) (CategoryTheory.CategoryStruct.id Z)
        (CategoryTheory.CategoryStruct.id X) ⋯ ⋯)
      (CategoryTheory.Limits.pushoutLeftPushoutInrIso X_1.hom f g).inv
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
aemeasurable_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [CompleteSpace F] [inst_4 : MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜]
  [inst_6 : MeasurableSpace F] [BorelSpace F] (f : 𝕜 → F) (μ : MeasureTheory.Measure 𝕜), AEMeasurable (deriv f) μ
-- Mathlib.Tactic.FunProp.Mor
/-- morphism argument  -/
Mathlib.Meta.FunProp.Mor.App.arg : Mathlib.Meta.FunProp.Mor.App → Lean.Expr
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
trapezoidal_integral.eq_1 : ∀ (f : ℝ → ℝ) (N : ℕ) (a b : ℝ),
  trapezoidal_integral f N a b =
    (b - a) / ↑N * ((f a + f b) / 2 + ∑ k ∈ Finset.range (N - 1), f (a + (↑k + 1) * (b - a) / ↑N))
-- Mathlib.Data.Multiset.Fintype
/-- There is some equivalence between `m` and `m.map f` which respects `f`.
 -/
Multiset.mapEquivAux : {α : Type u_1} →
  {β : Type u_2} →
    [inst : DecidableEq α] →
      [inst_1 : DecidableEq β] → (m : Multiset α) → (f : α → β) → Squash { v // ∀ (a : m.ToType), (v a).fst = f a.fst }
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.omega_ord : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → Ordinal.omega c.ord = c.ord
-- Mathlib.RingTheory.HahnSeries.Summable
/-- An elementwise scalar multiplication of one summable family on another.  -/
HahnSeries.SummableFamily.smul : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      {V : Type u_4} →
        {α : Type u_5} →
          {β : Type u_6} →
            [inst : PartialOrder Γ] →
              [inst_1 : PartialOrder Γ'] →
                [inst_2 : AddCommMonoid V] →
                  [inst_3 : AddCommMonoid R] →
                    [SMulWithZero R V] →
                      [inst_5 : VAdd Γ Γ'] →
                        [IsOrderedCancelVAdd Γ Γ'] →
                          HahnSeries.SummableFamily Γ R α →
                            HahnSeries.SummableFamily Γ' V β → HahnSeries.SummableFamily Γ' V (α × β)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Algebra.hom_ext_iff : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → Semiring (G i)] [inst_6 : (i : ι) → Algebra R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {P : Type u_7}
  [inst_9 : Semiring P] [inst_10 : Algebra R P] {g₁ g₂ : DirectLimit G f →ₐ[R] P},
  g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (DirectLimit.Algebra.of G f i) = g₂.comp (DirectLimit.Algebra.of G f i)
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The canonical truncation of a homological complex relative to an embedding
of complex shapes `e` which satisfies `e.IsTruncLE`.  -/
HomologicalComplex.truncLE' : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') → [e.IsTruncLE] → [∀ (i' : ι'), K.HasHomology i'] → HomologicalComplex C c
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.smul_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F] {f : X → E} {μ : MeasureTheory.VectorMeasure X F},
  μ.Integrable f → ∀ (c : ℝ), (c • μ).Integrable f
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoEquivHomologicalComplex_functor : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.dgoEquivHomologicalComplex b V).functor = HomologicalComplex.dgoToHomologicalComplex b V
-- Init.Data.Bool
Bool.if_true_left : ∀ (p : Prop) [h : Decidable p] (f : Bool), (if p then true else f) = (decide p || f)
-- Mathlib.Probability.Decision.Risk.Countable
ProbabilityTheory.avgRisk_countable' : ∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {κ : ProbabilityTheory.Kernel 𝓧 𝓨}
  {π : MeasureTheory.Measure Θ} [Countable 𝓨] [MeasurableSingletonClass 𝓨],
  Measurable ℓ → ProbabilityTheory.avgRisk ℓ P κ π = ∑' (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y * ((P θ).bind ⇑κ) {y} ∂π
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instPreservesColimitsOfShapeSchemeTopCatDiscreteForgetToTopOfSmall : ∀ {σ : Type v} [Small.{u, v} σ],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete σ) AlgebraicGeometry.Scheme.forgetToTop
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z)
  [inst_4 : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x (CategoryTheory.inv f))
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x z)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E},
  IsAlgebraic F α → F⟮α⟯.toSubalgebra = F[α]
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.go : ℤ → Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.of_fixedField_eq_bot : ∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E],
  IntermediateField.fixedField ⊤ = ⊥ → IsGalois F E
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_one_right_eq : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M : Submodule R S),
  M.mulMap (Subalgebra.toSubmodule ⊥) = M.subtype ∘ₗ ↑M.rTensorOne
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_comp_subtype : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {s : Set ι},
  AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ MvPolynomial.supported R s, (MvPolynomial.aeval x) p = 0 → p = 0
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U.eq_1 : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.U R 0 = 1
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.one_sub_eta_q_ne_zero : ∀ (n : ℕ) {z : ℂ}, z ∈ UpperHalfPlane.upperHalfPlaneSet → 1 - ModularForm.eta_q n z ≠ 0
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapIsoWhiskerLeft_inv : ∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (H : CategoryTheory.Functor C E) {Fᵣ Gᵣ : CategoryTheory.Functor D E'}
  (α : Fᵣ ≅ Gᵣ), (CategoryTheory.Join.mapIsoWhiskerLeft H α).inv = CategoryTheory.Join.mapWhiskerLeft H α.inv
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrKey.mk.inj : ∀ {relName head : Lean.Name} {arity : ℕ} {relName_1 head_1 : Lean.Name} {arity_1 : ℕ},
  { relName := relName, head := head, arity := arity } = { relName := relName_1, head := head_1, arity := arity_1 } →
    relName = relName_1 ∧ head = head_1 ∧ arity = arity_1
-- Mathlib.Probability.Martingale.OptionalStopping
MeasureTheory.smul_le_stoppedValue_hittingBtwn : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f 𝒢 μ →
    ∀ {ε : NNReal} (n : ℕ),
      ε • μ {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω} ≤
        ENNReal.ofReal
          (∫ (ω : Ω) in {ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun k => f k ω},
            MeasureTheory.stoppedValue f (fun ω => ↑(MeasureTheory.hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ)
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.instFormallyUnramified : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FormallyEtale R A], Algebra.FormallyUnramified R A
-- Std.Time.Date.PlainDate
/-- Creates a `PlainDate` by clipping the day to ensure validity. This function forces the date to be
valid by adjusting the day to fit within the valid range to fit the given month and year.
 -/
Std.Time.PlainDate.ofYearMonthDayClip : Std.Time.Year.Offset → Std.Time.Month.Ordinal → Std.Time.Day.Ordinal → Std.Time.PlainDate
-- Mathlib.Order.Cover
Prod.mk_covBy_mk_iff_right : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {a : α} {b₁ b₂ : β},
  (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.AddSaturated.iInf : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_2} {f : ι → AddSubmonoid M},
  (∀ (i : ι), (f i).AddSaturated) → (iInf f).AddSaturated
-- Mathlib.Order.Hom.Bounded
instCoeTCBotHomOfBotHomClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Bot α] [inst_2 : Bot β]
  [inst_3 : BotHomClass F α β], instCoeTCBotHomOfBotHomClass = { coe := BotHomClass.toBotHom }
-- Mathlib.Data.Num.Lemmas
Num.castNum_xor : ∀ (m n : Num), ↑(m ^^^ n) = ↑m ^^^ ↑n
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.CWComplex.Subcomplex.cell_def : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : T2Space X] [inst_1 : Topology.CWComplex C]
  (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ), Topology.RelCWComplex.cell (↑E) n = ↑(E.I n)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.hasCoeToTopCat : CoeOut AlgebraicGeometry.Scheme TopCat
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Given `c.p == .num k`
```
p = d.getPoly.normEq0 k
```
 -/
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0 : Lean.Grind.CommRing.Poly →
  Lean.Meta.Grind.Arith.CommRing.PolyDerivation →
    Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Meta.Grind.Arith.CommRing.PolyDerivation
-- Mathlib.RingTheory.Smooth.Kaehler
retractionOfSectionOfKerSqZero_comp_kerToTensor : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S] (g : S →ₐ[R] P)
  (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S),
  retractionOfSectionOfKerSqZero g hf' hg ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.submoduleMap_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f → ∀ (p : Submodule R M), Function.Injective ⇑(f.submoduleMap p)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.coe_ofContinuousOpenRestrict : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)) (hs : IsOpen e.source),
  ↑(OpenPartialHomeomorph.ofContinuousOpenRestrict e hc ho hs) = ↑e
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.comap_symm : ∀ {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (e : V ≃ W),
  SimpleGraph.comap (⇑e.symm.toEmbedding) G = SimpleGraph.map (⇑e.toEmbedding) G
-- Init.Data.List.Attach
List.attachWith_nil : ∀ {α : Type u_1} {P : α → Prop} {H : ∀ x ∈ [], P x}, [].attachWith P H = []
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.norm_kernel_le : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x y : X),
  ‖RKHS.kernel H x y‖ ≤ √‖RKHS.kernel H x x‖ * √‖RKHS.kernel H y y‖
-- Std.Http.Data.URI.Encoding
/-- Creates an `EncodedQueryString` from a `String` by checking if it's already a valid percent-encoded string.
Returns `some` if valid, `none` otherwise.
 -/
Std.Http.URI.EncodedQueryString.ofString? : String → (r : optParam (UInt8 → Bool) Std.Http.Internal.Char.isQueryChar) → Option (Std.Http.URI.EncodedQueryString r)
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.op_adj₁ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H), t.op.adj₁ = t.adj₂.op
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiable_of_subsingleton : ∀ {𝕜 : 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] [Subsingleton E] {f : E → F}, Differentiable 𝕜 f
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
DifferentiableAt.fderiv_restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F} {x : E},
  DifferentiableAt 𝕜' f x → fderiv 𝕜 f x = ContinuousLinearMap.restrictScalars 𝕜 (fderiv 𝕜' f x)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- `SMulWithZero` is a class consisting of a Type `M₀` with `0 ∈ M₀` and a scalar multiplication
of `M₀` on a Type `A` with `0`, such that the equality `r • m = 0` holds if at least one among `r`
or `m` equals `0`.  -/
SMulWithZero : (M₀ : Type u_2) → (A : Type u_7) → [Zero M₀] → [Zero A] → Type (max u_2 u_7)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsOpenImmersionMapOfHomForallEvalRingHom : ∀ {ι : Type u} (i : ι) (R : ι → Type (max u_1 u)) [inst : (i : ι) → CommRing (R i)],
  AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x => R x) i)))
-- Mathlib.Algebra.Ring.Subsemiring.Defs
AddSubmonoidWithOneClass.toOneMemClass : ∀ {S : Type u_1} {R : outParam (Type u_2)} {inst : AddMonoidWithOne R} {inst_1 : SetLike S R}
  [self : AddSubmonoidWithOneClass S R], OneMemClass S R
-- Mathlib.Analysis.Normed.Module.Bases
GeneralSchauderBasis.mk.inj : ∀ {β : Type u_3} {𝕜 : Type u_4} {X : Type u_5} {inst : NontriviallyNormedField 𝕜} {inst_1 : NormedAddCommGroup X}
  {inst_2 : NormedSpace 𝕜 X} {L : SummationFilter β} {basis : β → X} {coord : β → StrongDual 𝕜 X}
  {ortho : ∀ (i j : β), (coord i) (basis j) = Pi.single j 1 i}
  {expansion : ∀ (x : X), HasSum (fun i => (coord i) x • basis i) x L} {basis_1 : β → X} {coord_1 : β → StrongDual 𝕜 X}
  {ortho_1 : ∀ (i j : β), (coord_1 i) (basis_1 j) = Pi.single j 1 i}
  {expansion_1 : ∀ (x : X), HasSum (fun i => (coord_1 i) x • basis_1 i) x L},
  { basis := basis, coord := coord, ortho := ortho, expansion := expansion } =
      { basis := basis_1, coord := coord_1, ortho := ortho_1, expansion := expansion_1 } →
    basis = basis_1 ∧ coord = coord_1
-- Mathlib.Algebra.Category.AlgCat.Basic
algEquivIsoAlgebraIso_inv : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : Algebra R X]
  [inst_4 : Algebra R Y], algEquivIsoAlgebraIso.inv = TypeCat.ofHom fun i => i.toAlgEquiv
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.hom_id : ∀ {M : SemiNormedGrp₁}, ↑(SemiNormedGrp₁.Hom.hom (CategoryTheory.CategoryStruct.id M)) = NormedAddGroupHom.id M.carrier
-- Mathlib.Algebra.Group.Action.Pretransitive
Additive.addAction_isPretransitive : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid α] [inst_1 : MulAction α β] [MulAction.IsPretransitive α β],
  AddAction.IsPretransitive (Additive α) β
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.SameCycle.cycleOf_eq : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} [inst : DecidableRel f.SameCycle],
  f.SameCycle x y → f.cycleOf x = f.cycleOf y
-- Mathlib.Order.Category.Lat
_private.Mathlib.Order.Category.Lat.0.Lat.Hom.mk.injEq : ∀ {X Y : Lat} (hom' hom'_1 : LatticeHom ↑X ↑Y), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)], (t.erase k).get! k = default
-- Mathlib.ModelTheory.Basic
Equiv.toFun_inducedStructureEquiv_Symm : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] (e : M ≃ N),
  ⇑e.inducedStructureEquiv.symm = ⇑e.symm
-- Init.Data.BitVec.Lemmas
BitVec.concat_extractLsb'_getLsb : ∀ {w : ℕ} {x : BitVec (w + 1)}, (BitVec.extractLsb' 1 w x).concat (x.getLsb 0) = x
-- Lean.Compiler.CSimpAttr
Lean.Compiler.hasCSimpAttribute : Lean.Environment → Lean.Name → Bool
-- Lean.Server.Completion.CompletionCollectors
/-- `NameSet` where names are compared according to `cmpModPrivate`.
Helps speed up dot completion because it allows us to look up names without first having to
strip the private prefix from deep in the name, letting us reject most names without
having to scan the full name first.
 -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.NameSetModPrivate : Type
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.reflectDataValue : Lean.DataValue → Lean.Term
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvPFunctor.appendContents.eq_1 : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {β : Type u_1} {a : P.A} (f' : (P.drop.B a).Arrow α)
  (f : P.last.B a → β), P.appendContents f' f = TypeVec.splitFun f' f
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.UniformEquicontinuousOn.uniformContinuousOn_of_mem : ∀ {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {H : Set (β → α)} {S : Set β},
  H.UniformEquicontinuousOn S → ∀ {f : β → α}, f ∈ H → UniformContinuousOn f S
-- Mathlib.Order.Lattice
inf_lt_sup : ∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊓ b < a ⊔ b ↔ a ≠ b
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.periods_eq_zmultiples_widthInfty : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥𝒢.periods], 𝒢.periods = AddSubgroup.zmultiples 𝒢.widthInfty
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_non_aestronglyMeasurable_of_le : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  a ≤ b → ¬MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b)) → ∫ (x : ℝ) in a..b, f x ∂μ = 0
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Stats : Type
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
/-- **Alias** of `MeasureTheory.condLExp_finsetSum`. -/
MeasureTheory.condLExp_finset_sum : ∀ {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} (mΩ : MeasurableSpace Ω)
  (s : Finset ι) {X : ι → Ω → ENNReal},
  (∀ (i : ι), AEMeasurable (X i) P) → P⁻[∑ i ∈ s, X i | mΩ] =ᵐ[P] ∑ i ∈ s, P⁻[X i | mΩ]
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instLineDerivSMulComplex : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F], LineDerivSMul ℂ E (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.Algebra.Ring.Invertible
AddUnits.neg_mulRight : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {x : AddUnits R} {y : R}, -x.mulRight y = (-x).mulRight y
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] [inst_4 : AddZeroClass α] [inst_5 : AddZeroClass β]
  [inst_6 : AddZeroClass γ] [inst_7 : AddZeroClass δ] (f : γ →+o δ) (g : β →+o γ) (h : α →+o β),
  (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.smulCommClass_left : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {α : Type u_1}
  {β : Type u_2} [inst_3 : SMul A β] [inst_4 : SMul α β] [SMulCommClass A α β] (S : Subalgebra R A),
  SMulCommClass (↥S) α β
-- Mathlib.GroupTheory.Congruence.Defs
Con.hrec_on₂_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {cM : Con M} {cN : Con N}
  {φ : cM.Quotient → cN.Quotient → Sort u_4} (a : M) (b : N) (f : (x : M) → (y : N) → φ ↑x ↑y)
  (h : ∀ (x : M) (y : N) (x' : M) (y' : N), cM x x' → cN y y' → f x y ≍ f x' y'), Con.hrecOn₂ (↑a) (↑b) f h = f a b
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity_eq_zero_iff : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {x : R}, Polynomial.rootMultiplicity x p = 0 ↔ p.IsRoot x → p = 0