mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Basic
/-- The `noWs` parser requires that there is *no* whitespace between the preceding and following
parsers. For example, the parser `"foo" noWs "+"` parses `foo+` but not `foo +`.

This is almost the same as `"foo+"`, but using this parser will make `foo+` a token, which may cause
problems for the use of `"foo"` and `"+"` as separate tokens in other parsers.

This parser has arity 0 - it does not capture anything.  -/
Lean.Parser.checkNoWsBefore : optParam String "no space before" → Lean.Parser.Parser
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mrange.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F), MonoidHom.mrange f = (Submonoid.map f ⊤).copy (Set.range ⇑f) ⋯
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.hdcongrArg : ∀ {α : Sort u} {a a' : α} {β : (a' : α) → a = a' → Sort v} (h : a = a') (f : (a' : α) → (h : a = a') → β a' h),
  f a ⋯ ≍ f a' h
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- A subring integrally closed in a field is the intersection of valuation subrings
containing it.  -/
Subring.eq_iInf_of_isIntegrallyClosedIn : ∀ {K : Type u_3} [inst : Field K] {R : Subring K} [IsIntegrallyClosedIn (↥R) K], R = ⨅ V, (↑V).toSubring
-- Mathlib.Topology.Algebra.InfiniteSum.Module
ContinuousLinearEquiv.map_tsum : ∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂} {σ' : R₂ →+* R}
  [inst_8 : RingHomInvPair σ σ'] [inst_9 : RingHomInvPair σ' σ] {L : SummationFilter ι} [T2Space M] [T2Space M₂]
  {f : ι → M} (e : M ≃SL[σ] M₂), e (∑'[L] (z : ι), f z) = ∑'[L] (z : ι), e (f z)
-- Mathlib.LinearAlgebra.Matrix.IsDiag
/-- `(A ⊗ B).IsDiag` if both `A` and `B` are diagonal.  -/
Matrix.IsDiag.kronecker : ∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : MulZeroClass α] {A : Matrix m m α} {B : Matrix n n α},
  A.IsDiag → B.IsDiag → (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B).IsDiag
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.instHasOrthogonalProjectionOrthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [K.HasOrthogonalProjection], Kᗮ.HasOrthogonalProjection
-- Mathlib.Combinatorics.Additive.Dissociation
/-- A set is dissociated iff all its finite subsets have different sums.

This is an analog of linear independence in a vector space, but with the "scalars" restricted to
`0` and `±1`.  -/
AddDissociated : {α : Type u_1} → [AddCommGroup α] → Set α → Prop
-- Mathlib.CategoryTheory.Localization.Adjunction
/-- This is the dual statement to `Adjunction.isLocalization`.  -/
CategoryTheory.Adjunction.isLocalization' : ∀ {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₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) [G.Full] [G.Faithful],
  F.IsLocalization ((CategoryTheory.MorphismProperty.isomorphisms C₁).inverseImage F)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ_δ₀Iter' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : autoParam (n + i = m) CategoryTheory.SimplicialObject.σ_δ₀Iter'._auto_1),
  autoParam (↑j = ↑j' + i) CategoryTheory.SimplicialObject.σ_δ₀Iter'._auto_3 →
    CategoryTheory.CategoryStruct.comp (X.σ j) (X.δ₀Iter i ⋯) =
      CategoryTheory.CategoryStruct.comp (X.δ₀Iter i hi') (X.σ j')
-- Init.Prelude
HPow.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HPow α β γ
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.le_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : DegLex (α →₀ ℕ)},
  x ≤ y ↔
    Finsupp.degree (ofDegLex x) < Finsupp.degree (ofDegLex y) ∨
      Finsupp.degree (ofDegLex x) = Finsupp.degree (ofDegLex y) ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y)
-- Init.Control.Lawful.MonadAttach.Instances
instLawfulMonadAttachReaderTOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [LawfulMonadAttach m], LawfulMonadAttach (ReaderT ρ m)
-- Mathlib.FieldTheory.AlgebraicClosure
algebraicClosure_toSubalgebra : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  (algebraicClosure F E).toSubalgebra = integralClosure F E
-- Mathlib.Algebra.Order.SuccPred
strictAntiOn_of_add_one_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : One α]
  [inst_4 : SuccAddOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) < f a) → StrictAntiOn f s
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Construct the sphere with the given diameter.  -/
EuclideanGeometry.Sphere.ofDiameter : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [NormedSpace ℝ V] → [inst_2 : MetricSpace P] → [NormedAddTorsor V P] → P → P → EuclideanGeometry.Sphere P
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.add_prehaar_le_addIndex : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G} (K : TopologicalSpace.Compacts G),
  (interior U).Nonempty →
    MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K ≤ ↑(MeasureTheory.Measure.haar.addIndex ↑K ↑K₀)
-- Mathlib.Algebra.RingQuot
RingQuot.eq_liftAlgHom_comp_mkAlgHom : ∀ (S : Type uS) [inst : CommSemiring S] {A : Type uA} [inst_1 : Semiring A] [inst_2 : Algebra S A] {B : Type u₄}
  [inst_3 : Semiring B] [inst_4 : Algebra S B] {s : A → A → Prop} (f : RingQuot s →ₐ[S] B),
  f = (RingQuot.liftAlgHom S) ⟨f.comp (RingQuot.mkAlgHom S s), ⋯⟩
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDF_ne_top : ∀ {μ : ℝ} {v : NNReal} {x : ℝ}, ProbabilityTheory.gaussianPDF μ v x ≠ ⊤
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.mem_subgroupGalEquivSubgroupChar_iff : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [inst_3 : CommRing R]
  [inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] (χ : DirichletCharacter R n) (H : Subgroup Gal(K/ℚ)),
  χ ∈ OrderDual.ofDual ((IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar n K R) H) ↔
    ∀ σ ∈ H, χ ↑((IsCyclotomicExtension.Rat.galEquivZMod n K) σ) = 1
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_awayMap : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {e : ι} {f g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g)
  (a : HomogeneousLocalization.Away 𝒜 f),
  HomogeneousLocalization.val ((HomogeneousLocalization.awayMap 𝒜 hg hx) a) =
    (Localization.awayLift (algebraMap A (Localization (Submonoid.powers x))) f ⋯) (HomogeneousLocalization.val a)
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.tensorUnit_def : ∀ {C : Type u} [inst : CategoryTheory.Bicategory C] (X : C),
  CategoryTheory.MonoidalCategoryStruct.tensorUnit (X ⟶ X) = CategoryTheory.CategoryStruct.id X
-- Mathlib.Order.Preorder.Chain
IsChain.lt_of_not_ge : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  IsChain (fun x1 x2 => x1 ≤ x2) s → ∀ {x y : α}, x ∈ s → y ∈ s → ¬x ≤ y → y < x
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- maps every element of the W type to a canonical representative  -/
MvQPF.mRepr : {n : ℕ} → {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → (MvQPF.P F).M α → (MvQPF.P F).M α
-- Mathlib.Order.RelClasses
WellFoundedRelation.asymmetric : ∀ {α : Sort u_1} [inst : WellFoundedRelation α] {a b : α}, WellFoundedRelation.rel a b → ¬WellFoundedRelation.rel b a
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_sup : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (s t : Subring R) (f : R →+* S),
  Subring.map f (s ⊔ t) = Subring.map f s ⊔ Subring.map f t
-- Lean.Meta.Sorry
/-- If `e` is a sorry application, returns the sorry itself,
stripping off any arguments in case the `sorry` is standing in for a function.

For labeled sorries, includes the label information.
 -/
Lean.Expr.getSorry? : Lean.Expr → Option Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.edgeFinset_deleteEdges : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype ↑G.edgeSet] (s : Finset (Sym2 V))
  [inst_2 : Fintype ↑(G.deleteEdges ↑s).edgeSet], (G.deleteEdges ↑s).edgeFinset = G.edgeFinset \ s
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- If `X` is not a compact space, then `OnePoint X` is a connected space.  -/
OnePoint.instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PreconnectedSpace X] [NoncompactSpace X], ConnectedSpace (OnePoint X)
-- Mathlib.Order.RelSeries
RelSeries.append_assoc : ∀ {α : Type u_1} {r : SetRel α α} (p q w : RelSeries r) (hpq : (p.last, q.head) ∈ r) (hqw : (q.last, w.head) ∈ r),
  (p.append q hpq).append w ⋯ = p.append (q.append w hqw) ⋯
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.exists_distinguished_triangle_of_epi : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C},
  (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) →
    ∀ [inst_7 : CategoryTheory.Preadditive A] [ι.Full] [ι.Faithful] [ι.Additive],
      CategoryTheory.Triangulated.AbelianSubcategory.admissibleMorphism ι = ⊤ →
        ∀ {X₂ X₃ : A} (π : X₂ ⟶ X₃) [CategoryTheory.Epi π],
          ∃ X₁ i δ,
            CategoryTheory.Pretriangulated.Triangle.mk (ι.map i) (ι.map π) δ ∈
              CategoryTheory.Pretriangulated.distinguishedTriangles
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getLeFn : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → [Lean.Meta.Grind.Arith.Linear.MonadGetStruct m] → m Lean.Expr
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if the maximum number of case-splits has been reached.  -/
Lean.Meta.Grind.checkMaxCaseSplit : Lean.Meta.Grind.GoalM Bool
-- Init.Data.SInt.Lemmas
Int16.sub_self : ∀ (a : Int16), a - a = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_one_lt_right' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulLeftStrictMono α] (a : α) {b : α}, 1 < b → a < a * b
-- Init.Data.Vector.Erase
Vector.eraseIdx_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {k : ℕ} {h : k < n}, (Vector.replicate n a).eraseIdx k h = Vector.replicate (n - 1) a
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.of_pow_associated_of_prime : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p₁ p₂ : M} {k₁ k₂ : ℕ},
  Prime p₁ → Prime p₂ → 0 < k₁ → Associated (p₁ ^ k₁) (p₂ ^ k₂) → Associated p₁ p₂
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Mapping by `f` and then forgetting is the same as forgetting.  -/
CategoryTheory.Under.mapForget_eq : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y),
  (CategoryTheory.Under.map f).comp (CategoryTheory.Under.forget X) = CategoryTheory.Under.forget Y
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_C : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a).natTrailingDegree = 0
-- Mathlib.Algebra.Module.Equiv.Basic
/-- If `M` and `M₂` are linearly isomorphic then the two spaces of linear maps from `M` and `M₂` to
themselves are linearly isomorphic.

See `LinearEquiv.conjRingEquiv` for the isomorphism between endomorphism rings,
which works over a not necessarily commutative semiring.  -/
LinearEquiv.conj : {R₁' : Type u_12} →
  {R₂' : Type u_13} →
    {M₁' : Type u_20} →
      {M₂' : Type u_21} →
        [inst : CommSemiring R₁'] →
          [inst_1 : CommSemiring R₂'] →
            [inst_2 : AddCommMonoid M₁'] →
              [inst_3 : AddCommMonoid M₂'] →
                [inst_4 : Module R₁' M₁'] →
                  [inst_5 : Module R₂' M₂'] →
                    {σ₁'₂' : R₁' →+* R₂'} →
                      {σ₂'₁' : R₂' →+* R₁'} →
                        [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁'] →
                          [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] →
                            (M₁' ≃ₛₗ[σ₁'₂'] M₂') → Module.End R₁' M₁' ≃ₛₗ[σ₁'₂'] Module.End R₂' M₂'
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.restrictFreeVar.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} {β : Type u_5} [inst : DecidableEq α]
  (motive : (x : ℕ) → (x_1 : L.BoundedFormula α x) → (↥x_1.freeVarFinset → β) → Sort u_4) (_n : ℕ)
  (_f : ↥FirstOrder.Language.BoundedFormula.falsum.freeVarFinset → β)
  (h_1 :
    (_n : ℕ) →
      (_f : ↥FirstOrder.Language.BoundedFormula.falsum.freeVarFinset → β) →
        motive _n FirstOrder.Language.BoundedFormula.falsum _f)
  (h_2 :
    (_n : ℕ) →
      (t₁ t₂ : L.Term (α ⊕ Fin _n)) →
        (f : ↥(FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset → β) →
          motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂) f)
  (h_3 :
    (_n l : ℕ) →
      (R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin _n)) →
          (f : ↥(FirstOrder.Language.BoundedFormula.rel R ts).freeVarFinset → β) →
            motive _n (FirstOrder.Language.BoundedFormula.rel R ts) f)
  (h_4 : (_n : ℕ) → (φ₁ φ₂ : L.BoundedFormula α _n) → (f : ↥(φ₁.imp φ₂).freeVarFinset → β) → motive _n (φ₁.imp φ₂) f)
  (h_5 : (_n : ℕ) → (φ : L.BoundedFormula α (_n + 1)) → (f : ↥φ.all.freeVarFinset → β) → motive _n φ.all f),
  (match _n, FirstOrder.Language.BoundedFormula.falsum, _f with
    | _n, FirstOrder.Language.BoundedFormula.falsum, _f => h_1 _n _f
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂, f => h_2 _n t₁ t₂ f
    | _n, FirstOrder.Language.BoundedFormula.rel R ts, f => h_3 _n l R ts f
    | _n, φ₁.imp φ₂, f => h_4 _n φ₁ φ₂ f
    | _n, φ.all, f => h_5 _n φ f) =
    h_1 _n _f
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_roi : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : LT α]
  [DecidableLT α] [inst_6 : Std.PRange.UpwardEnumerable α] [inst_7 : Std.Rxi.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roi α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEquiv_dep_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α ≃ β} {D : Set β}, (M.mapEquiv f).Dep D ↔ M.Dep (⇑f.symm '' D)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.instEquivLike : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_6} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_9} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_10} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {n : WithTop ℕ∞} → EquivLike (Diffeomorph I I' M M' n) M M'
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.intermediateFieldEquivSubgroup_apply : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] [inst_5 : Finite G]
  {F : IntermediateField K L},
  (IsGaloisGroup.intermediateFieldEquivSubgroup G K L) F = OrderDual.toDual (fixingSubgroup G ↑F)
-- Mathlib.Order.Extension.Well
WellOrderExtension.wellFoundedLT : ∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedLT α], WellFoundedLT (WellOrderExtension α)
-- Mathlib.Algebra.ContinuedFractions.Determinant
_private.Mathlib.Algebra.ContinuedFractions.Determinant.0.GenContFract.determinant_aux : ∀ {K : Type u_1} [inst : Field K] {g : GenContFract K} {n : ℕ},
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    (g.contsAux n).a * (g.contsAux (n + 1)).b - (g.contsAux n).b * (g.contsAux (n + 1)).a =
      ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.elabCDotFunctionAlias?.expandCDotArg? : Lean.Term → Lean.MacroM (Option Lean.Term)
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesColimits.newCocone_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra}
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)),
  (CategoryTheory.Monad.ForgetCreatesColimits.newCocone c).ι =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Monad.ForgetCreatesColimits.γ c.ι
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.toLinearMap_intrinsicStar : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : ContinuousStar E]
  [inst_13 : ContinuousStar F] (f : WithConv (E →L[R] F)), ↑(star f).ofConv = (star (WithConv.toConv ↑f.ofConv)).ofConv
-- Mathlib.Data.Sum.Basic
Sum.elim_injective : ∀ {α : Type u} {β : Type v} {γ : Sort u_3} {f : α → γ} {g : β → γ},
  Function.Injective (Sum.elim f g) ↔ Function.Injective f ∧ Function.Injective g ∧ ∀ (a : α) (b : β), f a ≠ g b
-- Mathlib.Algebra.Group.Hom.Instances
OneHom.instMonoid.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : Monoid N],
  OneHom.instMonoid =
    { toMul := OneHom.instMul, mul_assoc := ⋯, toOne := instOneOneHom, one_mul := ⋯, mul_one := ⋯, toNPow := NPow.ofPow,
      npow_zero := ⋯, npow_succ := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β},
  Std.ExtDHashMap.Const.get? (m.insertIfNew k v) a =
    if (k == a) = true ∧ k ∉ m then some v else Std.ExtDHashMap.Const.get? m a
-- Lean.Meta.Tactic.Simp.Main
/-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal  -/
Lean.Meta.Simp.isOfNatNatLit : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.PreZeroHypercover.isSheafFor_iff_of_iso : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {S : C}
  {𝒰 𝒱 : CategoryTheory.PreZeroHypercover S} (e : 𝒰 ≅ 𝒱),
  CategoryTheory.Presieve.IsSheafFor F 𝒰.presieve₀ ↔ CategoryTheory.Presieve.IsSheafFor F 𝒱.presieve₀
-- Mathlib.CategoryTheory.Limits.Presentation
/-- Change the index category of a colimit presentation.  -/
CategoryTheory.Limits.ColimitPresentation.reindex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          CategoryTheory.Limits.ColimitPresentation J X →
            {J' : Type u_1} →
              [inst_2 : CategoryTheory.Category.{v_1, u_1} J'] →
                (F : CategoryTheory.Functor J' J) → [F.Final] → CategoryTheory.Limits.ColimitPresentation J' X
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.norm_coe_mul : ∀ (p x t : ℝ), ‖↑(t * x)‖ = |t| * ‖↑x‖
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.wEquiv.abs' : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x y : (MvQPF.P F).W α),
  MvQPF.abs ((MvQPF.P F).wDest' x) = MvQPF.abs ((MvQPF.P F).wDest' y) → MvQPF.WEquiv x y
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.add_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddZeroClass 𝕜] [inst_1 : LE α] (f g : IncidenceAlgebra 𝕜 α) (a b : α),
  (f + g) a b = f a b + g a b
-- Lean.IdentifierSuggestion
/-- Throw an unknown constant/identifier error message, potentially suggesting alternatives using
`suggest_for` attributes.

The replacement will mimic the path structure of the original as much as possible if they share a
path prefix: if there is a suggestion for replacing `Foo.Bar.jazz` with `Foo.Bar.baz`, then
`Bar.jazz` will be replaced by `Bar.baz` unless the resulting constant is ambiguous.
 -/
Lean.throwUnknownNameWithSuggestions : {α : Type} →
  (constName : Lean.Name) →
    optParam String "identifier" →
      optParam Lean.Name constName →
        optParam (Option Lean.Syntax) none → optParam Lean.MessageData Lean.MessageData.nil → Lean.Elab.TermElabM α
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.counit_coe_finsupp : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M : Type u_4}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : CoalgebraStruct R M] (x : n →₀ M),
  CoalgebraStruct.counit ⇑x = CoalgebraStruct.counit x
-- Mathlib.GroupTheory.OrderOfElement
AddCommute.addOrderOf_dvd_lcm_add : ∀ {G : Type u_1} [inst : AddMonoid G] {x y : G}, AddCommute x y → addOrderOf y ∣ (addOrderOf x).lcm (addOrderOf (x + y))
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Option.isSome.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((val : α) → motive (some val)) → (Unit → motive none) → motive x
-- Mathlib.Algebra.BigOperators.Finprod
finsum_def : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) [inst_1 : Decidable (Function.HasFiniteSupport f)],
  ∑ᶠ (i : α), f i = if h : Function.HasFiniteSupport f then ∑ i ∈ Set.Finite.toFinset h, f i else 0
-- Mathlib.RingTheory.SimpleModule.Isotypic
Submodule.linearEquiv_of_sSup_eq_top : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  [IsSimpleModule R ↥N] (s : Set (Submodule R M)) [h : ∀ (m : ↑s), IsSimpleModule R ↥↑m],
  sSup s = ⊤ → ∃ S ∈ s, Nonempty (↥N ≃ₗ[R] ↥S)