mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_forIn'_loop : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] {α : Type uu} (as : List α)
  (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (as' : List α) (b : β) (p : ∃ bs, bs ++ as' = as),
  Lean.Order.monotone f → Lean.Order.monotone fun x => List.forIn'.loop as (f x) as' b p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_eq_some_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.maxKey? = some (t.maxKeyD fallback)
-- Mathlib.Analysis.Normed.MulAction
Prod.instNormSMulClass : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddGroup β] [inst_2 : SMul α β]
  [NormSMulClass α β] {γ : Type u_3} [inst_4 : SeminormedAddGroup γ] [inst_5 : SMul α γ] [NormSMulClass α γ],
  NormSMulClass α (β × γ)
-- Mathlib.AlgebraicGeometry.Noetherian
/-- `R` is a Noetherian ring if and only if `Spec R` is a Noetherian scheme.  -/
AlgebraicGeometry.isNoetherian_Spec : ∀ {R : CommRingCat}, AlgebraicGeometry.IsNoetherian (AlgebraicGeometry.Spec R) ↔ IsNoetherianRing ↑R
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.closure_ball_subset_closedBall : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, closure (Metric.ball x ε) ⊆ Metric.closedBall x ε
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_toSubsemigroup : ∀ {M : Type u_2} [inst : AddZeroClass M] (H : AddSubmonoid Mᵃᵒᵖ), H.unop.toAddSubsemigroup = H.unop
-- Mathlib.ModelTheory.Basic
/-- An equivalence of first-order structures is an equivalence that commutes with the
interpretations of functions and relations.  -/
FirstOrder.«term_≃[_]_» : Lean.TrailingParserDescr
-- Mathlib.Tactic.Convert
/-- `ac_change t` on a goal `⊢ t'` changes the goal to `⊢ t` and adds new goals for proving the equality
`t' = t` using congruence, then tries proving these goals by associativity and commutativity. The
goals are created like `congr!` would.
In other words, `ac_change t` is like `convert_to t` followed by `ac_refl`.

Like `refine e`, any holes (`?_` or `?x`) in `t` that are not solved by unification are converted
into new goals, using the hole's name, if any, as the goal case name.
Like `congr!`, `convert_to` introduces variables while applying congruence rules. These can be
pattern-matched, like `rintro` would, using the `with` keyword.

* `ac_change! t` uses default transparency, rather than reducible, when solving side goals.
* `ac_change t using n`, where `n` is a positive numeral, controls the depth with which congruence
  is applied. For example, if the main goal is `⊢ Prime ((a * b + 1) + c)`,
  then `ac_change Prime ((1 + a * b) + c) using 2` solves the side goals, and
  `ac_change Prime ((1 + a * b) + c) using 3` (or more) results in two (impossible) goals
  `⊢ 1 = a * b` and `⊢ a * b = 1`.
  The default value for `n` is 1.

Example:
```lean
example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
  ac_change a + d + e + f + c + g + b ≤ _
  -- ⊢ a + d + e + f + c + g + b ≤ N
```
 -/
Mathlib.Tactic.acChange! : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffAt_iff_target_of_mem_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {y : M'}
  {n : WithTop ℕ∞} [IsManifold I' n M'],
  f x ∈ (chartAt H' y).source →
    (ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) x)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).getKey? k = if k ∈ m₂ then m₁.getKey? k else none
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
/-- A ball of radius `ε` on the unit sphere in a real normed space
has measure at least `toSphereBallBound n ε * μ (ball 0 1)`,
where `n` is the dimension of the space,
`toSphereBallBound n ε` is a lower estimate that depends only on the dimension and `ε`,
which is positive for positive `n` and `ε`.  -/
MeasureTheory.Measure.toSphereBallBound_mul_measure_unitBall_le_toSphere_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {ε : ℝ},
  0 < ε →
    ∀ (x : ↑(Metric.sphere 0 1)),
      ↑(MeasureTheory.Measure.toSphereBallBound (Module.finrank ℝ E) ε) * μ (Metric.ball 0 1) ≤
        μ.toSphere (Metric.ball x ε)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (hom : M.X ⟶ N.X)
  [isModHom : CategoryTheory.IsModHom A hom] (hom_1 : M.X ⟶ N.X) (isModHom_1 : CategoryTheory.IsModHom A hom_1),
  ({ hom := hom, isModHom := isModHom } = { hom := hom_1, isModHom := isModHom_1 }) = (hom = hom_1)
-- Aesop.Search.Main
Aesop.throwAesopEx : {Q : Type} →
  [inst : Aesop.Queue Q] →
    {α : Type} → Lean.MVarId → Array Lean.MVarId → Bool → Option Lean.MessageData → Aesop.SearchM Q α
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.ne_iff : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {f g : Π₀ (i : ι), β i}, f ≠ g ↔ ∃ i, f i ≠ g i
-- Init.Data.SInt.Lemmas
ISize.mul_neg : ∀ (a b : ISize), a * -b = -(a * b)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.withConstantsSelfStructure : (L : FirstOrder.Language) → {M : Type w} → [L.Structure M] → (L.withConstants M).Structure M
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield of a field inherits a field structure  -/
SubfieldClass.toField : {S : Type u_1} → {K : Type u_2} → [inst : Field K] → [inst_1 : SetLike S K] → [SubfieldClass S K] → (s : S) → Field ↥s
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.Spec.birdDet.match_1.splitter : {R : Type u_1} →
  (motive : (n : ℕ) → Matrix (Fin n) (Fin n) R → Sort u_2) →
    (n : ℕ) →
      (A : Matrix (Fin n) (Fin n) R) →
        ((A : Matrix (Fin 0) (Fin 0) R) → motive 0 A) →
          ((k : ℕ) → (A : Matrix (Fin (k + 1)) (Fin (k + 1)) R) → motive k.succ A) → motive n A
-- Mathlib.Geometry.Manifold.Instances.Sphere
continuous_stereoInvFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1),
  Continuous (stereoInvFun hv)
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.projIdx.sizeOf_spec : ∀ (structName : Lean.Name) (idx : ℕ),
  sizeOf (Lean.Elab.Term.LValResolution.projIdx structName idx) = 1 + sizeOf structName + sizeOf idx
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.inner_comm_comm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (x y : TensorProduct 𝕜 E F), inner 𝕜 ((TensorProduct.comm 𝕜 E F) x) ((TensorProduct.comm 𝕜 E F) y) = inner 𝕜 x y
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The image of X in a `StandardEtalePresentation`.  -/
StandardEtalePresentation.x : {R : Type u_4} →
  {S : Type u_5} →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → StandardEtalePresentation R S → S
-- Mathlib.Tactic.Linarith.Verification
/-- `proveFalseByLinarith` is the main workhorse of `linarith`.
Given a list `l` of proofs of `tᵢ Rᵢ 0`,
it tries to derive a contradiction from `l` and use this to produce a proof of `False`.

`oracle : CertificateOracle` is used to search for a certificate of unsatisfiability.

The returned certificate is a map `m` from hypothesis indices to natural number coefficients.
If our set of hypotheses has the form `{tᵢ Rᵢ 0}`,
then the elimination process should have guaranteed that
1.\ `∑ (m i)*tᵢ = 0`,
with at least one `i` such that `m i > 0` and `Rᵢ` is `<`.

We have also that
2.\ `∑ (m i)*tᵢ < 0`,
since for each `i`, `(m i)*tᵢ ≤ 0` and at least one is strictly negative.
So we conclude a contradiction `0 < 0`.

It remains to produce proofs of (1) and (2). (1) is verified by calling the provided `discharger`
tactic, which is typically `ring`. We prove (2) by folding over the set of hypotheses.

`transparency : TransparencyMode` controls the transparency level with which atoms are identified.
 -/
Mathlib.Tactic.Linarith.proveFalseByLinarith : Lean.Meta.TransparencyMode →
  Mathlib.Tactic.Linarith.CertificateOracle →
    Lean.Elab.Tactic.TacticM Unit → Lean.MVarId → List Lean.Expr → Lean.MetaM (Lean.Expr × List ℕ)
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The type `(shrinkYoneda.obj X).obj Y` is equivalent to `Y.unop ⟶ X`.  -/
CategoryTheory.shrinkYonedaObjObjEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      {X : C} → {Y : Cᵒᵖ} → (CategoryTheory.shrinkYoneda.{w, v, u}.obj X).obj Y ≃ (Opposite.unop Y ⟶ X)
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.instPreservesFiniteLimitsFunctorObjWhiskeringLeftOfHasFiniteLimits : ∀ {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] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.HasFiniteLimits E],
  CategoryTheory.Limits.PreservesFiniteLimits ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The affine open cover given by a covering family of affine opens.  -/
AlgebraicGeometry.Scheme.AffineOpenCover.ofIsOpenCover : {X : AlgebraicGeometry.Scheme} →
  {ι : Type u_1} →
    (U : ι → X.Opens) →
      TopologicalSpace.IsOpenCover U → (∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)) → X.AffineOpenCover
-- Mathlib.Algebra.Ring.ULift
ULift.semiring : {R : Type u} → [Semiring R] → Semiring (ULift.{u_1, u} R)
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.coe_ideal_le_self_mul_inv : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] (I : Ideal R₁), ↑I ≤ ↑I * (↑I)⁻¹
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_counitIso_hom_app_right_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L'))
  (X_1 : D),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).counitIso.hom.app X).right.app X_1 =
    CategoryTheory.CategoryStruct.id (X.right.obj X_1)
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
LinearMap.rTensor_exact_iff_lTensor_exact : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} (Q : Type u_5)
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] {f : M →ₗ[R] N}
  {g : N →ₗ[R] P},
  Function.Exact ⇑(LinearMap.rTensor Q f) ⇑(LinearMap.rTensor Q g) ↔
    Function.Exact ⇑(LinearMap.lTensor Q f) ⇑(LinearMap.lTensor Q g)
-- Mathlib.Tactic.FunProp.FunctionData
/-- Of the form `⇑f x` i.e. morphism and one argument is provided.  -/
Mathlib.Meta.FunProp.MorApplication.exact : Mathlib.Meta.FunProp.MorApplication
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- This is the inverse of the previous construction: a cocone of an extended functor
`liftFromUnder.obj K : WithInitial J ⥤ C` consists of an object of `C`, together
with morphisms. This same object is a cocone of the original functor `K : J ⥤ Under X`.  -/
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeBack : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          {K : CategoryTheory.Functor J (CategoryTheory.Under X)} →
            CategoryTheory.Functor (CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K))
              (CategoryTheory.Limits.Cocone K)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsSingular.cof_ord_lt : ∀ {c : Cardinal.{u_1}}, c.IsSingular → c.ord.cof < c
-- Init.Data.BitVec.Lemmas
BitVec.append_of_zero_width : ∀ {w v : ℕ} (x : BitVec w) (y : BitVec v) (h : w = 0), x ++ y = BitVec.cast ⋯ y
-- Mathlib.Topology.Sheaves.PresheafOfFunctions
/-- The presheaf of continuous functions on `X` with values in fixed target topological space
`T`.  -/
TopCat.presheafToTop : (X : TopCat) → TopCat → TopCat.Presheaf (Type u_1) X
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {k a : α} {v : β k}
  {h₁ : (m.insert k v).contains a = true}, (m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.Context.mk.inj : ∀ {env : Lean.Environment} {checkReducible checkProj : Bool} {env_1 : Lean.Environment}
  {checkReducible_1 checkProj_1 : Bool},
  { env := env, checkReducible := checkReducible, checkProj := checkProj } =
      { env := env_1, checkReducible := checkReducible_1, checkProj := checkProj_1 } →
    env = env_1 ∧ checkReducible = checkReducible_1 ∧ checkProj = checkProj_1
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
Set.rangeSplitting.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (x : ↑(Set.range f)), Set.rangeSplitting f x = Exists.choose ⋯
-- Mathlib.Tactic.Push
Mathlib.Tactic.Push.Config.mk.inj : ∀ {distrib distrib_1 : Bool}, { distrib := distrib } = { distrib := distrib_1 } → distrib = distrib_1
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.val.inj : ∀ {e e_1 : Lean.Expr}, Lean.Meta.Match.Pattern.val e = Lean.Meta.Match.Pattern.val e_1 → e = e_1
-- Lean.Meta.Tactic.Grind.EMatch
/-- This constraint is used to encode multi-patterns.  -/
Lean.Meta.Grind.EMatch.Cnstr.continue : Lean.Expr → Lean.Meta.Grind.EMatch.Cnstr
-- Mathlib.Algebra.Order.ToIntervalMod
AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, ¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b
-- Mathlib.RingTheory.Smooth.Kaehler
isScalarTower_of_section_of_ker_sqZero : ∀ {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),
  RingHom.ker (algebraMap P S) ^ 2 = ⊥ →
    (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S → IsScalarTower P S ↥(RingHom.ker (algebraMap P S))
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationBy.body : Lean.Elab.TerminationBy → Lean.Term
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientSubgroupOfMapOfLE_apply_mk : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (H : Subgroup α) (h : s ≤ t) (g : ↥H),
  Subgroup.quotientSubgroupOfMapOfLE H h ↑g = ↑g
-- Mathlib.Algebra.Jordan.Basic
CommSemigroup.isCommJordan : ∀ (A : Type u_1) [inst : CommSemigroup A], IsCommJordan A
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_subset_cons : ∀ {α : Type u_1} {a : α} {s t : Multiset α}, s ⊆ t → a ::ₘ s ⊆ a ::ₘ t
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.base_isIso_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [CategoryTheory.IsIso f], CategoryTheory.IsIso f.base
-- Mathlib.CategoryTheory.Action.Continuous
/-- Restricting scalars along a composition is naturally isomorphic to restricting scalars twice.  -/
ContAction.resComp : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              {G : Type u_4} →
                [inst_4 : Monoid G] →
                  [inst_5 : TopologicalSpace G] →
                    {H : Type u_5} →
                      [inst_6 : Monoid H] →
                        [inst_7 : TopologicalSpace H] →
                          {K : Type u_6} →
                            [inst_8 : Monoid K] →
                              [inst_9 : TopologicalSpace K] →
                                (f : G →ₜ* H) →
                                  (h : H →ₜ* K) →
                                    ContAction.res V (h.comp f) ≅ (ContAction.res V h).comp (ContAction.res V f)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- The stabilizer of a set acts on that set.  -/
SMul.ofStabilizer : (G : Type u_1) →
  [inst : Group G] → (α : Type u_2) → [inst_1 : MulAction G α] → (s : Set α) → SMul ↥(MulAction.stabilizer G s) ↑s
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.uncenteredCovarianceBilinDual.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} [inst_1 : NormedSpace ℝ E]
  [inst_2 : OpensMeasurableSpace E] (μ μ_1 : MeasureTheory.Measure E),
  μ = μ_1 → ProbabilityTheory.uncenteredCovarianceBilinDual μ = ProbabilityTheory.uncenteredCovarianceBilinDual μ_1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Add to the `todo` stack all matches that result from a `.star` in the query expression.
 -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.matchQueryStar : {α : Type} →
  Lean.Meta.RefinedDiscrTree.TrieIndex →
    Lean.Meta.RefinedDiscrTree.PartialMatch✝ →
      Array Lean.Meta.RefinedDiscrTree.PartialMatch✝ →
        optParam ℕ 1 → Lean.Meta.RefinedDiscrTree.TreeM✝ α (Array Lean.Meta.RefinedDiscrTree.PartialMatch✝)
-- Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
/-- A slightly stronger version of `exists_partition` on which we perform induction on `n`:
for all `ε > 0`, we can partition the remainders of any family of polynomials `A`
into equivalence classes, where the equivalence(!) relation is "closer than `ε`".  -/
Polynomial.exists_partition_polynomial_aux : ∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Field Fq] (n : ℕ) {ε : ℝ},
  0 < ε →
    ∀ {b : Polynomial Fq},
      b ≠ 0 →
        ∀ (A : Fin n → Polynomial Fq),
          ∃ t,
            ∀ (i₀ i₁ : Fin n),
              t i₀ = t i₁ ↔ ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'.loop.match_3.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.Torsor.Defs
/-- `v ↦ v • p` as an equivalence.  -/
Equiv.smulConst : {G : Type u_1} → {P : Type u_2} → [inst : Group G] → [Torsor G P] → P → G ≃ P
-- Mathlib.Algebra.Order.Module.Defs
PosSMulStrictMono.toPosSMulMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : PartialOrder α]
  [inst_4 : PartialOrder β] [PosSMulStrictMono α β], PosSMulMono α β
-- Mathlib.Algebra.Group.WithOne.Map
WithOne.map₂_eq_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : WithOne α} {b : WithOne β},
  WithOne.map₂ f a b = 1 ↔ a = 1 ∨ b = 1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} [inst_3 : Inhabited (β k)], (m₁.union m₂).get! k = m₂.getD k (m₁.get! k)
-- Mathlib.Algebra.Group.Invertible.Defs
/-- `1` is the inverse of itself  -/
invertibleOne : {α : Type u} → [inst : Monoid α] → Invertible 1
-- Mathlib.Order.Disjoint
eq_top_of_bot_isCompl : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x : α}, IsCompl ⊥ x → x = ⊤
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Restriction of an `AddMonoidHom` to an `AddSubmonoid` of the domain.  -/
AddMonoidHom.domRestrict : {M : Type u_1} →
  [inst : AddZeroClass M] →
    {N : Type u_5} →
      {S : Type u_6} →
        [inst_1 : AddZeroClass N] →
          [inst_2 : SetLike S M] → [inst_3 : AddSubmonoidClass S M] → (M →+ N) → (s : S) → ↥s →+ N
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- `∀ᵐ a, p a` means that `p a` for a.e. `a`, i.e. `p` holds true away from a null set.

This is notation for `Filter.Eventually P (MeasureTheory.ae MeasureSpace.volume)`.  -/
MeasureTheory.«term∀ᵐ_,_» : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_comp_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F},
  ContDiff 𝕜 (↑n) f → ∀ (c : 𝕜), (iteratedDeriv n fun x => f (c * x)) = fun x => c ^ n • iteratedDeriv n f (c * x)
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.left_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (n : N),
  (SemidirectProduct.inl n).left = n
-- Lean.Data.Trie
Lean.Data.Trie.node.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : Option α) (a_1 : ByteArray) (a_2 : Array (Lean.Data.Trie α)),
  sizeOf (Lean.Data.Trie.node a a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.of_constantCoeff_zero : ∀ {τ : Type u_3} {S : Type u_4} [inst : CommRing S] {a : MvPowerSeries τ S},
  MvPowerSeries.constantCoeff a = 0 → PowerSeries.HasSubst a
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodCartan.eq_1 : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {R : Type u_5} [inst_4 : CommRing R] [inst_5 : LieAlgebra R L₁]
  {H₁ : LieSubalgebra R L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_6 : LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂}
  (b₂ : LieAlgebra.Basis ι₂ H₂),
  LieAlgebra.Basis.prodCartan✝ eι b₁ b₂ =
    LieSubalgebra.lieSpan R ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂) {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x}
-- Mathlib.GroupTheory.Index
AddSubgroup.index_map_subtype : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} (K : AddSubgroup ↥H),
  (AddSubgroup.map H.subtype K).index = K.index * H.index