mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.IsRootSystem.span_coroot_eq_top : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N}
  [self : P.IsRootSystem], Submodule.span R (Set.range ⇑P.coroot) = ⊤
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.zero_ne_bot : ∀ {α : Type u} [inst : Zero α], 0 ≠ ⊥
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addZeroClass : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddZeroClass (f i)] → AddZeroClass ((i : I) → f i)
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.RefIdentJsonRepr.c.injEq : ∀ (m n m_1 n_1 : String),
  (Lean.Lsp.RefIdent.RefIdentJsonRepr.c m n = Lean.Lsp.RefIdent.RefIdentJsonRepr.c m_1 n_1) = (m = m_1 ∧ n = n_1)
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommMonoidWithTop.isAddLeftRegular_of_ne_top : ∀ {α : Type u_3} [self : LinearOrderedAddCommMonoidWithTop α] ⦃x : α⦄, x ≠ ⊤ → IsAddLeftRegular x
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.toRange_app_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (p : F' ⟶ F) {i : C}
  (x : F'.obj i),
  ↑((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Subfunctor.toRange p).app i)) x) =
    (CategoryTheory.ConcreteCategory.hom (p.app i)) x
-- Init.Data.List.Find
List.findIdx?_append : ∀ {α : Type u_1} {xs ys : List α} {p : α → Bool},
  List.findIdx? p (xs ++ ys) = (List.findIdx? p xs).or (Option.map (fun i => i + xs.length) (List.findIdx? p ys))
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.GeometricallyIrreducible.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.geometrically (fun x => IrreducibleSpace ↥x) f → AlgebraicGeometry.GeometricallyIrreducible f
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_sub_left' : ∀ {α : Type u} [inst : Ring α] (x y : α), Ideal.span {y - x, y} = Ideal.span {x, y}
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The hard part of the Lusin separation theorem saying that two disjoint analytic sets are
contained in disjoint Borel sets (see the full statement in `AnalyticSet.measurablySeparable`).
Here, we prove this when our analytic sets are the ranges of functions from `ℕ → ℕ`.
 -/
MeasureTheory.measurablySeparable_range_of_disjoint : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α] [inst_2 : MeasurableSpace α] [OpensMeasurableSpace α]
  {f g : (ℕ → ℕ) → α},
  Continuous f →
    Continuous g → Disjoint (Set.range f) (Set.range g) → MeasureTheory.MeasurablySeparable (Set.range f) (Set.range g)
-- Mathlib.Algebra.Group.Action.End
/-- The tautological additive action by `Additive (Function.End α)` on `α`.  -/
Function.End.applyAddAction : {α : Type u_5} → AddAction (Additive (Function.End α)) α
-- Lean.Parser.Attr
Lean.Parser.Attr.class : Lean.Parser.Parser
-- Mathlib.Tactic.Module
/-- Given expressions `R` and `M` representing types such that `M`'s is a module over `R`'s, and
given two terms `l₁`, `l₂` of type `qNF R M`, i.e. lists of `(Q($R) × Q($M)) × ℕ`s (two `Expr`s
and a natural number), construct a list of new goals: that the `R`-coefficient of an `M`-atom which
appears in only one list is zero, and that the `R`-coefficients of an `M`-atom which appears in both
lists are equal.  Also construct (dependent on these new goals) a proof that the "linear
combinations" represented by `l₁` and `l₂` are equal in `M`.  -/
Mathlib.Tactic.Module.reduceCoefficientwise : {u v : Lean.Level} →
  {M : Q(Type v)} →
    {R : Q(Type u)} →
      {x : Q(AddCommMonoid «$M»)} →
        {x_1 : Q(Semiring «$R»)} →
          (iRM : Q(Module «$R» «$M»)) →
            (l₁ l₂ : Mathlib.Tactic.Module.qNF R M) →
              Lean.MetaM
                (List Lean.MVarId ×
                  have a := l₂.toNF;
                  have a_1 := l₁.toNF;
                  Q(«$a_1».eval = «$a».eval))
-- Mathlib.Algebra.Order.Hom.TypeTags
/-- Reinterpret `G ≃*o H` as `Additive G ≃+o Additive H`.  -/
OrderMonoidIso.toAdditive : {G : Type u_1} →
  {H : Type u_2} →
    [inst : CommMonoid G] →
      [inst_1 : PartialOrder G] →
        [inst_2 : CommMonoid H] → [inst_3 : PartialOrder H] → (G ≃*o H) ≃ (Additive G ≃+o Additive H)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_right_le_size_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₂.size ≤ (m₁ ∪ m₂).size
-- Init.Core
iff_def' : ∀ {a b : Prop}, (a ↔ b) ↔ (b → a) ∧ (a → b)
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The colimit of `F ⋙ forget₂ CommSemiRingCat SemiRingCat` in the category `SemiRingCat`.
In the following, we will show that this has the structure of a _commutative_ semiring.
 -/
CommSemiRingCat.FilteredColimits.R : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J CommSemiRingCat → SemiRingCat
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A `C^n` local diffeomorphism is differentiable.  -/
IsLocalDiffeomorph.mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N},
  IsLocalDiffeomorph I J n f → n ≠ 0 → MDiff f
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_comap : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (φ : L.Hom M N)
  (S : L.Substructure N), ↑(FirstOrder.Language.Substructure.comap φ S) = ⇑φ ⁻¹' ↑S
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
Finsupp.addSingleEquiv.congr_simp : ∀ {R : Type u_4} {ι : Type u_6} [inst : Ring R] (i i_1 : ι) (e_i : i = i_1) (c c_1 : ι → R) (e_c : c = c_1)
  (h₀ : c i = 0), Finsupp.addSingleEquiv i c h₀ = Finsupp.addSingleEquiv i_1 c_1 ⋯
-- Mathlib.Order.WithBot
WithBot.le_iff_forall : ∀ {α : Type u_1} [inst : LE α] {x y : WithBot α}, x ≤ y ↔ ∀ (a : α), x = ↑a → ∃ b, y = ↑b ∧ a ≤ b
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddHom.eqLocus.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f g : M →ₙ+ N),
  f.eqLocus g = { carrier := {x | f x = g x}, add_mem' := ⋯ }
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.trans.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S')
  {E'' : Type u_5} [inst_4 : Group E''] {S'' : GroupExtension N E'' G} (equiv' : S'.Equiv S''),
  equiv.trans equiv' = { toMulEquiv := equiv.trans equiv'.toMulEquiv, inl_comm := ⋯, rightHom_comm := ⋯ }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_left_le_size_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.size ≤ (t₁ ∪ t₂).size
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.op_smul_set_subset_mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a : α}, a ∈ t → MulOpposite.op a • s ⊆ s * t
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).maxKey ⋯ = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.subset_adjoin : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (s : Set A), s ⊆ ↑(NonUnitalStarAlgebra.adjoin R s)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Square C),
  CategoryTheory.CategoryStruct.comp self.f₁₂ self.f₂₄ = CategoryTheory.CategoryStruct.comp self.f₁₃ self.f₃₄
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_top_smul_measure : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive (⊤ • μ) T C) (f : α → E),
  MeasureTheory.setToFun (⊤ • μ) T hT f = 0
-- Mathlib.LinearAlgebra.Finsupp.Span
Finsupp.iInf_ker_lapply_le_bot : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⨅ a, (Finsupp.lapply a).ker ≤ ⊥
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₆_of_isCharNeTwoNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF], W.b₆ = 4 * W.a₆
-- Mathlib.AlgebraicGeometry.FunctionField
/-- For `f` an element of the function field of `X`, there exists some open set `U ⊆ X` such that
`f` is a unit in `Γ(X, U)`.
 -/
AlgebraicGeometry.exists_isUnit_germ_eq : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsIntegral X] (f : ↑X.functionField),
  f ≠ 0 →
    ∃ U ∈ X.affineOpens,
      ∃ f', ∃ (x : Nonempty ↥↑U), (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f' = f ∧ IsUnit f'
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- A version of `WithBot.map` for `AddMonoidHom`s.  -/
AddMonoidHom.withBotMap : {M : Type u_1} →
  {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → (M →+ N) → WithBot M →+ WithBot N
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_fst : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2], ⇑AffineMap.fst = Prod.fst
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan_mul_cos : ∀ {x : ℂ}, Complex.cos x ≠ 0 → Complex.tan x * Complex.cos x = Complex.sin x
-- Std.Data.TreeSet.AdditionalOperations
/-- Given a proof that such an element exists, retrieves the smallest element that is
less than the given element.
 -/
Std.TreeSet.getLT : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] → (t : Std.TreeSet α cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → α
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.HasOxfordStrings.emp : {α : Sort u_1} → [self : Lean.HasOxfordStrings✝ α] → α
-- Mathlib.Data.Fin.Rev
Fin.rev_eq_iff : ∀ {n : ℕ} {i j : Fin n}, i.rev = j ↔ i = j.rev
-- Mathlib.Data.Multiset.Basic
Multiset.toList_eq_singleton_iff : ∀ {α : Type u_1} {a : α} {m : Multiset α}, m.toList = [a] ↔ m = {a}
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.num.sizeOf_spec : ∀ (v : ℤ), sizeOf (Int.Internal.Linear.Expr.num v) = 1 + sizeOf v
-- Mathlib.Data.Int.ModEq
Dvd.dvd.modEq_zero_int : ∀ {n a : ℤ}, n ∣ a → a ≡ 0 [ZMOD n]
-- Mathlib.Data.Set.Image
Set.range_inl_inter_range_inr : ∀ {α : Type u_1} {β : Type u_2}, Set.range Sum.inl ∩ Set.range Sum.inr = ∅
-- Mathlib.Order.RelClasses
instIsWellOrderProdLex : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s],
  IsWellOrder (α × β) (Prod.Lex r s)
-- Lean.Linter.Deprecated
Lean.Linter.deprecatedAttr : Lean.ParametricAttribute Lean.Linter.DeprecationEntry
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.ppPHashSet : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [Lean.ToMessageData α] → Lean.PHashSet α → Lean.MessageData
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.inv_apply : ∀ (G : Type u_4) [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [inst_2 : MeasurableInv G],
  ⇑(MeasurableEquiv.inv G) = Inv.inv
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_quotient_add_rank_le : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial R]
  (M' : Submodule R M), Module.rank R (M ⧸ M') + Module.rank R ↥M' ≤ Module.rank R M
-- Mathlib.Data.Setoid.Basic
/-- Equivalence between functions `α → β` such that `r x y → f x = f y` and functions
`quotient r → β`.  -/
Setoid.liftEquiv : {α : Type u_1} → {β : Type u_2} → (r : Setoid α) → { f // r ≤ Setoid.ker f } ≃ (Quotient r → β)
-- Init.Data.UInt.Lemmas
USize.ofNat_le_iff : ∀ {n : USize} {m : ℕ}, m < USize.size → (USize.ofNat m ≤ n ↔ m ≤ n.toNat)
-- Mathlib.Algebra.Group.Hom.Instances
OneHom.instZPow.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : Group N],
  OneHom.instZPow = { pow := fun f n => { toFun := ⇑f ^ n, map_one' := ⋯ } }
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- The ring homomorphism from the stalk of the structure sheaf of `Proj` at a point corresponding
to a homogeneous prime ideal `x` to the *homogeneous localization* at `x`,
formed by gluing the `openToLocalization` maps.  -/
AlgebraicGeometry.stalkToFiberRingHom : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (x : ↑(ProjectiveSpectrum.top 𝒜)) →
                (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.stalk x ⟶
                  CommRingCat.of (HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.RootOrdered.eq_def : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : RBTree.RBNode.Path α) (x_1 : α),
  RBTree.RBNode.Path.RootOrdered cmp x x_1 =
    match x, x_1 with
    | RBTree.RBNode.Path.root, x => True
    | RBTree.RBNode.Path.left c parent x r, v =>
      RBTree.RBNode.cmpLT cmp v x ∧ RBTree.RBNode.Path.RootOrdered cmp parent v
    | RBTree.RBNode.Path.right c l x parent, v =>
      RBTree.RBNode.cmpLT cmp x v ∧ RBTree.RBNode.Path.RootOrdered cmp parent v
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'ToRestriction_naturality_assoc : ∀ {ι : 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 L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i'] {Z : HomologicalComplex C c}
  (h : L.restriction e ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLE'Map φ e)
      (CategoryTheory.CategoryStruct.comp (L.truncLE'ToRestriction e) h) =
    CategoryTheory.CategoryStruct.comp (K.truncLE'ToRestriction e)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap φ e) h)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.divModByMonicAux.eq_def : ∀ {R : Type u} [inst : Ring R] (x x_1 : Polynomial R) (x_2 : x_1.Monic),
  x.divModByMonicAux x_2 =
    match x, x_1, x_2 with
    | p, q, hq =>
      if h : q.degree ≤ p.degree ∧ p ≠ 0 then
        have z := Polynomial.C p.leadingCoeff * Polynomial.X ^ (p.natDegree - q.natDegree);
        have _wf := ⋯;
        have dm := (p - q * z).divModByMonicAux hq;
        (z + dm.1, dm.2)
      else (0, p)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.leftRightHomologyComparison'_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData),
  CategoryTheory.ShortComplex.leftRightHomologyComparison' h.left h.right = h.iso.hom
-- Lean.MetavarContext
/-- "Eliminate" the given variables `xs` from the context of the metavariable represented `mvarId`
by returning the application of a new metavariable whose type abstracts the forward dependencies
on `xs` after restricting it to the free variables in the local context of `mvarId`.

See details in the comment at the top of the file.
 -/
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.elimMVar : Array Lean.Expr → Lean.MVarId → Array Lean.Expr → Bool → Lean.MetavarContext.MkBinding.M (Lean.Expr × Array Lean.Expr)
-- Mathlib.Order.SupClosed
infClosed_empty : ∀ {α : Type u_3} [inst : SemilatticeInf α], InfClosed ∅
-- Mathlib.Data.Set.NAry
Set.image2_subset_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β},
  t ⊆ t' → Set.image2 f s t ⊆ Set.image2 f s t'
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
/-- The `Weyl group` of a root pairing is the group of automorphisms of the root pairing generated
by reflections.  -/
RootPairing.weylGroup : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → Subgroup P.Aut
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → k ∉ t₁ ∩ t₂
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {m n : ℕ} (s : Affine.Simplex k P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)), (s.reindex e).closedInterior = s.closedInterior
-- Lean.Elab.Term.TermElabM
/-- The kind of a tactic metavariable, used for additional error reporting.  -/
Lean.Elab.Term.TacticMVarKind : Type
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_self_add_right : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddGroup (N a)] (f g : Π₀ (a : α), N a), f.neLocus (f + g) = g.support
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- Return the `apply` tactic that performs the application.  -/
_private.Mathlib.Tactic.ClickSuggestions.Apply.0.Mathlib.Tactic.ClickSuggestions.tacticSyntax : Mathlib.Tactic.ClickSuggestions.Premise → Lean.Expr → Bool → Bool → Lean.MetaM (Lean.TSyntax `tactic)
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.orderIsoOfPrime_apply_coe : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (p : { p // p.IsPrime }),
  ↑((IsLocalization.orderIsoOfPrime M S) p) = Ideal.under R ↑p
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.toQuotient_map_apply : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A) (x : relations.R →₀ A),
  relations.toQuotient (relations.map x) = 0
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.comp_apply : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B]
  [inst_4 : Monoid C] [inst_5 : Star C] (f : B →⋆* C) (g : A →⋆* B) (a : A), (f.comp g) a = f (g a)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- An additive group object is an additive monoid object.  -/
CategoryTheory.AddGrp.toAddMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.AddGrp C → CategoryTheory.AddMon C
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
/-- A sub star semigroup is a subset of a magma which is closed under the `star`.  -/
SubStarSemigroup : (M : Type v) → [Mul M] → [Star M] → Type v
-- Mathlib.Lean.Expr.Basic
/-- Returns `true` if `type` is an application of a constant `decl` for which `p decl` is true, or a
forall with return type of the same form (i.e. of the form `∀ (x₀ : X₀) (x₁ : X₁) ⋯, decl ..` where
`p decl`).

Runs `cleanupAnnotations` on `type` and `forallE` bodies, and ignores metadata in applications.
 -/
Lean.Expr.isAppOrForallOfConstP : (Lean.Name → Bool) → Lean.Expr → Bool
-- Mathlib.Algebra.Polynomial.Homogenize
/-- **Alias** of `Polynomial.isHomogeneous_toTupleMvPolynomial`. -/
Polynomial.isHomogenous_toTupleMvPolynomial : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (i : Fin 2),
  (p.toTupleMvPolynomial i).IsHomogeneous p.natDegree
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence.  -/
CategoryTheory.Under.homMk_comp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V W : CategoryTheory.Under X}
  (f : U.right ⟶ V.right) (g : V.right ⟶ W.right) (w_f : CategoryTheory.CategoryStruct.comp U.hom f = V.hom)
  (w_g : CategoryTheory.CategoryStruct.comp V.hom g = W.hom),
  CategoryTheory.Under.homMk (CategoryTheory.CategoryStruct.comp f g) ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.homMk f w_f) (CategoryTheory.Under.homMk g w_g)
-- Init.Data.UInt.Lemmas
UInt32.sub_le : ∀ {a b : UInt32}, b ≤ a → a - b ≤ a
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Conjugating a function to write it in the preferred charts around `x`.
The manifold derivative of `f` will just be the derivative of this conjugated function.  -/
writtenInExtChartAt : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {M : Type u_3} →
      {H : Type u_4} →
        {E' : Type u_5} →
          {M' : Type u_6} →
            {H' : Type u_7} →
              [inst : NontriviallyNormedField 𝕜] →
                [inst_1 : NormedAddCommGroup E] →
                  [inst_2 : NormedSpace 𝕜 E] →
                    [inst_3 : TopologicalSpace H] →
                      [inst_4 : TopologicalSpace M] →
                        ModelWithCorners 𝕜 E H →
                          [inst_5 : NormedAddCommGroup E'] →
                            [inst_6 : NormedSpace 𝕜 E'] →
                              [inst_7 : TopologicalSpace H'] →
                                [inst_8 : TopologicalSpace M'] →
                                  ModelWithCorners 𝕜 E' H' →
                                    [ChartedSpace H M] → [ChartedSpace H' M'] → M → (M → M') → E → E'
-- Batteries.Tactic.GeneralizeProofs
/-- Core implementation of `abstractProofs`.
 -/
_private.Batteries.Tactic.GeneralizeProofs.0.Batteries.Tactic.GeneralizeProofs.abstractProofs.visit : Lean.Expr → Option Lean.Expr → Batteries.Tactic.GeneralizeProofs.MAbs Lean.Expr
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zag.refl : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] (X : J), CategoryTheory.Zag X X
-- Init.Data.Array.Basic
/-- Removes the element at a given index from an array without a run-time bounds check.

This function takes worst-case `O(n)` time because it back-shifts all elements at positions
greater than `i`.

Examples:
* `#["apple", "pear", "orange"].eraseIdx 0 = #["pear", "orange"]`
* `#["apple", "pear", "orange"].eraseIdx 1 = #["apple", "orange"]`
* `#["apple", "pear", "orange"].eraseIdx 2 = #["apple", "pear"]`
 -/
Array.eraseIdx : {α : Type u} → (xs : Array α) → (i : ℕ) → autoParam (i < xs.size) Array.eraseIdx._auto_1 → Array α
-- Mathlib.Topology.ClusterPt
mem_closure_iff_nhds' : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, x ∈ closure s ↔ ∀ t ∈ nhds x, ∃ y, ↑y ∈ t
-- Mathlib.NumberTheory.MulChar.Basic
/-- We can convert a multiplicative character into a homomorphism of monoids with zero when
the source has a zero and another element.  -/
MulChar.toMonoidWithZeroHom : {R' : Type u_2} →
  [inst : CommMonoidWithZero R'] →
    {R : Type u_3} → [inst_1 : CommMonoidWithZero R] → [Nontrivial R] → MulChar R R' → R →*₀ R'
-- Mathlib.GroupTheory.Focal
Subgroup.focalSubgroupOf_def : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.focalSubgroupOf = H.focalSubgroup.subgroupOf H