mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.AtTopBot.Field
Filter.tendsto_const_mul_pow_atTop : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ},
  n ≠ 0 → 0 < c → Filter.Tendsto (fun x => c * x ^ n) Filter.atTop Filter.atTop
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Finite measures yield elements of the `WeakDual` of bounded continuous nonnegative
functions via `MeasureTheory.FiniteMeasure.testAgainstNN`, i.e., integration.  -/
MeasureTheory.FiniteMeasure.toWeakDualBCNN : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : TopologicalSpace Ω] →
      [OpensMeasurableSpace Ω] → MeasureTheory.FiniteMeasure Ω → WeakDual NNReal (BoundedContinuousFunction Ω NNReal)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_set_eq_nat_iff_finset : ∀ {α : Type u_1} {s : Set α} {n : ℕ}, Cardinal.mk ↑s = ↑n ↔ ∃ t, ↑t = s ∧ t.card = n
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_mul_single_one : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] (x : MonoidAlgebra R M) (r : R) (m : M),
  (x * MonoidAlgebra.single 1 r).coeff m = x.coeff m * r
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_singleton_eq_range : ∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (y : M),
  ↑(R ∙ y) = Set.range fun x => x • y
-- Std.Data.DTreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.DTreeMap.toArray : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Array ((a : α) × β a)
-- Mathlib.CategoryTheory.Subfunctor.Sieves
CategoryTheory.Subfunctor.sieveOfSection_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (G : CategoryTheory.Subfunctor F) {U : Cᵒᵖ} (s : F.obj U) (V : C) (f : V ⟶ Opposite.unop U),
  (G.sieveOfSection s).arrows f = ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) s ∈ G.obj (Opposite.op V))
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.noZeroDivisors : ∀ {R : Type u_3} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided] [hI : I.IsPrime], NoZeroDivisors (R ⧸ I)
-- Mathlib.Data.Set.List
Set.range_list_get : ∀ {α : Type u_1} (l : List α), Set.range l.get = {x | x ∈ l}
-- Mathlib.Algebra.GroupWithZero.Basic
mul_eq_right₀ : ∀ {M₀ : Type u_1} {a b : M₀} [inst : MulZeroOneClass M₀] [IsRightCancelMulZero M₀], b ≠ 0 → (a * b = b ↔ a = 1)
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_mul : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a b : ℚ),
  Lean.Grind.Field.NormNum.ofRat (a * b) = Lean.Grind.Field.NormNum.ofRat a * Lean.Grind.Field.NormNum.ofRat b
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompIso_comp_id : ∀ {C₀ : Type u_1} {C₁ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] {F₀₁ : CategoryTheory.Functor C₀ C₁}
  {F₁₁' : CategoryTheory.Functor C₁ C₁} {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₁'₁ : CategoryTheory.Functor C₁ C₁}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₁' : F₁₁' ⊣ G₁'₁) (e₀₁₁' : G₁'₁.comp G₁₀ ≅ G₁₀) (e₁'₁ : G₁'₁ ≅ CategoryTheory.Functor.id C₁),
  e₀₁₁' = CategoryTheory.Functor.isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor →
    adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ e₀₁₁' = F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor
-- Lean.Meta.Tactic.Rewrite
/-- Rewrite `e` using `heq` in the context of `mvarId`.
Returns the result of the rewrite, the metavariable `mvarId` is not assigned.
 -/
Lean.MVarId.rewrite : Lean.MVarId →
  Lean.Expr →
    Lean.Expr → optParam Bool false → optParam Lean.Meta.Rewrite.Config { } → Lean.MetaM Lean.Meta.RewriteResult
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.getKeyGT?.go : {α : Type u} → {β : α → Type v} → [Ord α] → α → Option α → Std.DTreeMap.Internal.Impl α β → Option α
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The counit of the adjunction `lightCondSetToSequential ⊣ sequentialToLightCondSet`
is an isomorphism.

Note: for now, we only have `ℕ∪{∞}` as a light profinite set at universe level 0, which is why we
can only prove this for `X : Sequential.{0}`.
 -/
LightCondSet.sequentialAdjunctionCounitIso : (X : Sequential) → LightCondSet.lightCondSetToSequential.obj (LightCondSet.sequentialToLightCondSet.obj X) ≅ X
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.IsUltra.isTrans_closedBall : ∀ {X : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : Zero R] [inst_2 : SemilatticeSup R] (d : PseudoMetric X R)
  [d.IsUltra] {ε : R}, SetRel.IsTrans {xy | d xy.1 xy.2 ≤ ε}
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_finCongr_Ioo : ∀ {n m : ℕ} (h : n = m) (i j : Fin n),
  Finset.map (finCongr h).toEmbedding (Finset.Ioo i j) = Finset.Ioo (Fin.cast h i) (Fin.cast h j)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Restrict the codomain of an algebra homomorphism.  -/
AlgHom.codRestrict : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R B] → (f : A →ₐ[R] B) → (S : Subalgebra R B) → (∀ (x : A), f x ∈ S) → A →ₐ[R] ↥S
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_closure_iff : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {x : R},
  x ∈ NonUnitalSubsemiring.closure s ↔ x ∈ AddSubmonoid.closure ↑(Subsemigroup.closure s)
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.eventuallyle : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) [inst_1 : NormedSpace ℂ E] (z : ℂ),
  BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
    DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1) →
      z ∈ Complex.HadamardThreeLines.verticalStrip 0 1 →
        (fun x => ‖f z‖) ≤ᶠ[nhdsWithin 0 (Set.Ioi 0)] fun ε =>
          ‖(↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 0)) ^ (1 - z) *
              (↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 1)) ^ z‖
-- Mathlib.AlgebraicGeometry.Sites.Representability
/-- The map from `X i` to the glued scheme `(glueData hf).glued`  -/
AlgebraicGeometry.Scheme.LocalRepresentability.toGlued : {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} →
  {ι : Type u} →
    {X : ι → AlgebraicGeometry.Scheme} →
      {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} →
        (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) →
          (i : ι) → X i ⟶ (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).glued
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.mapOfCompatibleSMul.congr_simp : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_22) (S : Type u_23) (M : Type u_24) (N : Type u_25)
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  [inst_5 : CommSemiring A] [inst_6 : Module A M] [inst_7 : Module A N] [inst_8 : SMulCommClass R A M]
  [inst_9 : CommSemiring S] [inst_10 : Module S M] [inst_11 : SMulCommClass R S M] [inst_12 : SMulCommClass A S M]
  [inst_13 : TensorProduct.CompatibleSMul R A M N],
  TensorProduct.mapOfCompatibleSMul R A S M N = TensorProduct.mapOfCompatibleSMul R A S M N
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.instInhabitedSubtypeFG : {R : Type u_1} →
  {M : Type u_2} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Inhabited { P // P.FG }
-- Init.Data.SInt.Lemmas
Int8.div_self : ∀ {a : Int8}, a / a = if a = 0 then 0 else 1
-- Init.Data.Option.Attach
/-- This lemma identifies maps over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
Option.map_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {o : Option { x // p x }} {f : { x // p x } → β} {g : α → β},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Option.map f o = Option.map g o.unattach
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.mk'.eq_1 : ∀ {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.AddMonObj A] {M N : CategoryTheory.AddMod D A} (f : M.X ⟶ N.X)
  (smul_hom :
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
        CategoryTheory.AddModObj.vadd),
  CategoryTheory.AddMod.Hom.mk' f smul_hom = { hom := f, isAddModHom := ⋯ }
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.exists_mem_propSetWithTop : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular] (a : ↑J.withTop.obj), ∃ S, J.PropSetWithTop κ' S ∧ a ∈ S
-- Init.Data.SInt.Bitwise
Int32.toInt64_xor : ∀ (a b : Int32), (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange.congr_simp : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f f_1 : M → N) (e_f : f = f_1)
  (hf : f 0 = 0) (g g_1 : α →₀ M), g = g_1 → Finsupp.mapRange f hf g = Finsupp.mapRange f_1 ⋯ g_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul_nc.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Mon → Sort u_1) (m₁ : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit)
  (h_2 : (pw : Lean.Grind.CommRing.Power) → motive (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit))
  (h_3 :
    (pw : Lean.Grind.CommRing.Power) → (m₁ : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult pw m₁)),
  m₁ = Lean.Grind.CommRing.Mon.unit →
    (match m₁ with
      | Lean.Grind.CommRing.Mon.unit => h_1 ()
      | Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit => h_2 pw
      | Lean.Grind.CommRing.Mon.mult pw m₁ => h_3 pw m₁) ≍
      h_1 ()
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHomClass.map_comp_comulAlgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] [inst_3 : Semiring B] [inst_4 : Bialgebra R B] [inst_5 : FunLike F A B]
  [inst_6 : BialgHomClass F R A B] (f : F),
  (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f
-- Mathlib.SetTheory.Ordinal.Family
/-- The type of ordinals in universe `u` is not `Small.{u}`. This is the type-theoretic analog of
the Burali-Forti paradox.  -/
not_small_ordinal : ¬Small.{u, max (u + 1) (v + 1)} Ordinal.{max u v}
-- Init.Data.Nat.Div.Basic
Nat.mul_div_mul_left : ∀ {m : ℕ} (n k : ℕ), 0 < m → m * n / (m * k) = n / k
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∉ t → (f t[k]?).isNone = true → (t.alter k f).size = t.size
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_natCast : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (n : ℕ), (↑n).toEnd = ↑n
-- Mathlib.RingTheory.GradedAlgebra.Radical
Ideal.IsHomogeneous.isPrime_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : CommRing A] [inst_1 : AddCommMonoid ι] [inst_2 : LinearOrder ι]
  [IsOrderedCancelAddMonoid ι] [inst_4 : SetLike σ A] [inst_5 : AddSubmonoidClass σ A] {𝒜 : ι → σ}
  [inst_6 : GradedRing 𝒜] {I : Ideal A},
  Ideal.IsHomogeneous 𝒜 I →
    (I.IsPrime ↔
      I ≠ ⊤ ∧ ∀ {x y : A}, SetLike.IsHomogeneousElem 𝒜 x → SetLike.IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sign_touchpointWeights_singleton_neg : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  {i j : Fin (n + 1)}, i ≠ j → SignType.sign (s.touchpointWeights {i} j i) = -1
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_lt_div_iff_left : ∀ {a b c : ENNReal}, c ≠ 0 → c ≠ ⊤ → (a / c < b / c ↔ a < b)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size
-- Mathlib.Algebra.Homology.ComplexShapeSigns
TotalComplexShapeSymmetry.symm : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  {c₁₂ : ComplexShape I₁₂} {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₂ c₁ c₁₂}
  [self : TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂), c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run `grind +suggestions` at every step in proofs, reporting where it succeeds.  -/
linter.tacticAnalysis.tryAtEachStepGrindSuggestions : Lean.Option Bool
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_clm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {G : Type u_2} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
  {c : 𝕜 → F →L[𝕜] G} {u : 𝕜 → F},
  DifferentiableAt 𝕜 c x →
    DifferentiableAt 𝕜 u x → deriv (fun y => (c y) (u y)) x = (deriv c x) (u x) + (c x) (deriv u x)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.apply_order_ne_zero' : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F}, p.order ≠ 0 → p p.order ≠ 0
-- Lean.Elab.PreDefinition.EqnsUtils
_private.Lean.Elab.PreDefinition.EqnsUtils.0.Lean.Elab.Eqns.whnfAux : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.RelSeries
/-- If a relation on `α` is infinite dimensional, then `α` is nonempty.  -/
RelSeries.nonempty_of_infiniteDimensional : ∀ {α : Type u_1} {r : SetRel α α} [r.InfiniteDimensional], Nonempty α
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.symm : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x y : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F x y → RingCat.Colimits.Relation F y x
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.instFiniteRepr : ∀ (R : Type u) [inst : Ring R] (x : FGModuleRepr R), Module.Finite R x.repr
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Measurable.comp_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} [inst : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} [inst_1 : MeasurableSpace δ] {f : α → δ} {g : δ → β},
  Measurable g → AEMeasurable f μ → AEMeasurable (g ∘ f) μ
-- Mathlib.CategoryTheory.Idempotents.Basic
CategoryTheory.Idempotents.isIdempotentComplete_iff_opposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  CategoryTheory.IsIdempotentComplete Cᵒᵖ ↔ CategoryTheory.IsIdempotentComplete C
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.toOrderIso_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), f.toOrderIso = ↑f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- A pushout cocone on `f` and `g` is determined by morphisms `inl : Y ⟶ W` and `inr : Z ⟶ W` such
that `f ≫ inl = g ↠ inr`.  -/
CategoryTheory.Limits.PushoutCocone.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {W : C} →
            (inl : Y ⟶ W) →
              (inr : Z ⟶ W) →
                CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr →
                  CategoryTheory.Limits.PushoutCocone f g
-- Mathlib.GroupTheory.GroupAction.Basic
/-- To prove inclusion of a *subgroup* in a stabilizer, it is enough to prove inclusions.  -/
AddAction.le_stabilizer_iff_vadd_le : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] (s : Set α) (H : AddSubgroup G),
  H ≤ AddAction.stabilizer G s ↔ ∀ g ∈ H, g +ᵥ s ⊆ s
-- Mathlib.Data.Set.Card
/-- Given a finite set `s`, the number of subsets of `s` with cardinality `n` is
`s.ncard.choose n`. See also `Finset.card_powersetCard`.  -/
Set.ncard_powerset_ncard : ∀ {α : Type u_1} {s : Set α}, s.Finite → ∀ (n : ℕ), {t | t ⊆ s ∧ t.ncard = n}.ncard = s.ncard.choose n
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_subset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t u : Finset α}, s / t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x / y ∈ u
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instZero : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} → [inst : AddCommMonoid M] → [inst_1 : TopologicalSpace M] → Zero (MeasureTheory.VectorMeasure α M)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_eq_getD_back?_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {fallback : α},
  t.maxKeyD fallback = t.keysArray.back?.getD fallback
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.eq_1 : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α → β),
  Isometry f = ∀ (x1 x2 : α), edist (f x1) (f x2) = edist x1 x2
-- Mathlib.Dynamics.Flow
Flow.coe_restrict_apply : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (ϕ : Flow τ α) {s : Set α} (h : IsInvariant ϕ.toFun s) (t : τ) (x : ↑s), ↑((ϕ.restrict h).toFun t x) = ϕ.toFun t ↑x
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCompleteSpace : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  CompleteSpace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.instNonemptySectionState : ∀ {α : Type}, Nonempty (Mathlib.Tactic.ClickSuggestions.SectionState α)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.go.eq_1 : ∀ {α : Type u_1} (sep : Array α) (a : List α) (a_1 : Array α), List.intercalateTR.go✝ sep a [] a_1 = a_1.toListAppend a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constInsertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {l : List (α × β)},
          (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t₁ l)).Equiv
            ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t₂ l)
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.add : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f g : ℝ → F},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → AbsolutelyContinuousOnInterval (f + g) a b
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The inverse of an isomorphism is an isomorphism.  -/
AddEquiv.symm : {M : Type u_9} → {N : Type u_10} → [inst : Add M] → [inst_1 : Add N] → M ≃+ N → N ≃+ M
-- Mathlib.Probability.Density
MeasureTheory.HasPDF.aemeasurable : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} (X : Ω → E)
  (ℙ : MeasureTheory.Measure Ω) (μ : MeasureTheory.Measure E) [MeasureTheory.HasPDF X ℙ μ], AEMeasurable X ℙ
-- Mathlib.GroupTheory.OrderOfElement
addSubmonoidOfIdempotent.eq_1 : ∀ {M : Type u_6} [inst : AddLeftCancelMonoid M] [inst_1 : Finite M] (S : Set M) (hS1 : S.Nonempty) (hS2 : S + S = S),
  addSubmonoidOfIdempotent S hS1 hS2 = { carrier := S, add_mem' := ⋯, zero_mem' := ⋯ }
-- Init.Data.Float.Float
/-- Efficiently computes `x * 2^i`.

This function does not reduce in the kernel.
 -/
Float.scaleB : Float → ℤ → Float
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.norm_def : ∀ {α : Type u_1} {R : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : Zero α]
  [inst_3 : NormedAddCommGroup R] (f : ContinuousMapZero α R), ‖f‖ = ‖↑f‖
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instNatCastHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → NatCast (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
/-- If `J` is a subcanonical precoverage, isomorphisms are local on the target for `J`.  -/
CategoryTheory.Precoverage.ZeroHypercover.instIsLocalAtTargetIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [J.toGrothendieck.Subcanonical] [CategoryTheory.Limits.HasPullbacks C] [J.IsStableUnderBaseChange],
  (CategoryTheory.MorphismProperty.isomorphisms C).IsLocalAtTarget J
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.evaluation_aut_surjective_of_isGalois : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C)
  [CategoryTheory.PreGaloisCategory.IsGalois A] (a : (F.obj A).obj),
  Function.Surjective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) a
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.flip.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {mM : MulOneClass M} {mN : MulOneClass N} {mP : CommMonoid P}
  (f : M →* N →* P),
  f.flip =
    { toFun := fun y => { toFun := fun x => (f x) y, map_one' := ⋯, map_mul' := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
infEDist_smul₀ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [NormSMulClass 𝕜 E] {c : 𝕜},
  c ≠ 0 → ∀ (s : Set E) (x : E), Metric.infEDist (c • x) (c • s) = ‖c‖₊ • Metric.infEDist x s
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.mk : {n : Type u_1} → {R : Type u₂} → (i j : n) → i ≠ j → R → Matrix.TransvectionStruct n R
-- Init.Data.List.Monadic
List.foldlM_map : ∀ {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} [inst : Monad m] {f : β₁ → β₂}
  {g : α → β₂ → m α} {l : List β₁} {init : α},
  List.foldlM g init (List.map f l) = List.foldlM (fun x y => g x (f y)) init l
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.alter_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, m.alter k f = ∅ ↔ (m = ∅ ∨ m.size = 1 ∧ k ∈ m) ∧ f (m.get? k) = none
-- Std.Tactic.Do.Syntax
/-- `mrevert` is like `revert`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ P → R := by
  mintro ⟨HP, HQ, HR⟩
  mrevert HR
  mrevert HP
  mintro HP'
  mintro HR'
  mexact HR'
```
 -/
Lean.Parser.Tactic.mrevert : Lean.ParserDescr
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- The ground set  -/
IndepMatroid.E : {α : Type u_2} → IndepMatroid α → Set α
-- Mathlib.Topology.MetricSpace.Thickening
Metric.hasBasis_nhdsSet_thickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {K : Set α},
  IsCompact K → (nhdsSet K).HasBasis (fun δ => 0 < δ) fun δ => Metric.thickening δ K
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.hasSmallLocalizedHom_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [L.IsLocalization W] {X Y : C},
  CategoryTheory.Localization.HasSmallLocalizedHom W X Y ↔ Small.{w, v₂} (L.obj X ⟶ L.obj Y)